1 /-
2 Copyright (c) 2018 Mario Carneiro. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Mario Carneiro
5
6 The partial recursive functions are defined similarly to the primitive
7 recursive functions, but now all functions are partial, implemented
8 using the `roption` monad, and there is an additional operation, called
9 μ-recursion, which performs unbounded minimization.
10 -/
11 import computability.primrec data.pfun
src └───────────────────┘ └───────┘
12
13 open encodable denumerable roption
14
15 namespace nat
16
17 section rfind
18 parameter (p : ℕ →. bool)
id ┴ └┘ └──┘
src ┴ └┘ └──┘
typ ┴ └┘ └──┘
doc └┘
19
20 private def lbp (m n : ℕ) : Prop := m = n + 1 ∧ ∀ k ≤ n, ff ∈ p k
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
21
22 parameter (H : ∃ n, tt ∈ p n ∧ ∀ k < n, (p k).dom)
id ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ └┘ ┴ ┴ ┴ └─┘
typ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
23
24 private def wf_lbp : well_founded lbp :=
id └──────────┘ └─┘
src └──────────┘ └─┘
typ └──────────┘ └─┘
25 ⟨let ⟨n, pn⟩ := H in begin
id └─┘ ┴
typ └─┘ ┴
st └─────
26 suffices : ∀m k, n ≤ k + m → acc (lbp p) k,
id ┴ ┴ ┴ └─┘ └─┘ ┴
src └─────────┘ └─┘ ┴ ┴┴┴ ┴┴┴ ┴ ┴└─┘┴ └─┘┴ └┘
typ └─────────┘ └─┘ ┴┴┴┴┴ ┴┴┴ ┴ ┴└─┘┴ └─┘┴┴└┘
doc └─────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt └─────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └─────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid └───────┘└┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────┘└─
27 { from λa, this _ _ (nat.le_add_left _ _) },
id └──┘ └─────────────┘
src └───┘ └─┘ └───┘ └─────────────┘└────┘
typ └───┘ └─┘└──┘└───┘ └─────────────┘└────┘
doc └───┘ └─┘ └───┘ └────┘
txt └───┘ └─┘ └───┘ └────┘
par └───┘ └─┘ └───┘ └────┘
pid └───┘ └─┘ └───┘ └───┘┴
st ───┘└──────────────────────────────────────┘└┘└
28 intros m k kn,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ──────────────┘└─
29 induction m with m IH generalizing k;
id ┴
src └────────┘ └───────────────────────┘
typ └────────┘┴└───────────────────────┘
doc └────────┘ └───────────────────────┘
txt └────────┘ └───────────────────────┘
par └────────┘ └───────────────────────┘
pid ┴ ┴└───────┘└─────────────┘
st ────────────────────────────────────────
30 refine ⟨_, λ y r, _⟩; rcases r with ⟨rfl, a⟩,
id ┴
src └─────┘ └─┘ └──────┘ └─────┘ └────────────┘
typ └─────┘ └─┘ └──────┘ └─────┘┴└────────────┘
doc └─────┘ └─┘ └──────┘ └─────┘ └────────────┘
txt └─────┘ └─┘ └──────┘ └─────┘ └────────────┘
par └─────┘ └─┘ └──────┘ └─────┘ └────────────┘
pid ┴ └─┘ └──────┘ ┴ └────────────┘
st ───────────────────────────────────────────────┘└─
31 { injection mem_unique pn.1 (a _ kn) },
id └────────┘ └┘ ┴ └┘
src └────────┘└────────┘┴ └─┘ └─┘ └┘
typ └────────┘└────────┘┴└┘└─┘ ┴└─┘└┘└┘
doc └────────┘ ┴ └─┘ └─┘ └┘
txt └────────┘ ┴ └─┘ └─┘ └┘
par └────────┘ ┴ └─┘ └─┘ └┘
pid ┴ ┴ └─┘ └─┘ ┴┴
st ───┘└─────────────────────────────────┘└┘└
32 { exact IH _ (by rw nat.add_right_comm; exact kn) }
id └┘ └────────────────┘ └┘
src └────┘ └─┘ ┴└─┘└────────────────┘└──────┘ └┘
typ └────┘└┘└─┘ ┴└─┘└────────────────┘└──────┘└┘└┘
doc └────┘ └─┘ ┴└─┘ └──────┘ └┘
txt └────┘ └─┘ ┴└─┘ └──────┘ └┘
par └────┘ └─┘ ┴└─┘ └──────┘ └┘
pid ┴ └─┘ └──┘ └──────┘ ┴┴
st ─────────────────┘└──────────────────────────────┘└┘└─
33 end⟩
st ──┘
34
35 def rfind_x : {n // tt ∈ p n ∧ ∀m < n, ff ∈ p m} :=
id ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ └┘ ┴ ┴ └┘ ┴
typ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
36 suffices ∀ k, (∀n < k, ff ∈ p n) → {n // tt ∈ p n ∧ ∀m < n, ff ∈ p m},
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
37 from this 0 (λ n, (nat.not_lt_zero _).elim),
id └──┘ ┴ └─────────────┘ └──┘
src └─────────────┘ └──┘
typ └──┘ ┴ └─────────────┘ └──┘
38 @well_founded.fix _ _ lbp wf_lbp begin
id └──────────────┘ └─┘ └────┘
src └──────────────┘ └─┘ └────┘
typ └──────────────┘ └─┘ └────┘
st └─────
39 intros m IH al,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───────────────┘└─
40 have pm : (p m).dom,
id ┴ ┴
src └────────┘ ┴ └───┘
typ └────────┘ ┴┴┴└───┘
doc └────────┘ ┴ └───┘
txt └────────┘ ┴ └───┘
par └────────┘ ┴ └───┘
pid └─────┘└─┘ ┴ └──┘┴
st ────────────────────┘└─
41 { rcases H with ⟨n, h₁, h₂⟩,
id ┴
src └─────┘ └───────────────┘
typ └─────┘┴└───────────────┘
doc └─────┘ └───────────────┘
txt └─────┘ └───────────────┘
par └─────┘ └───────────────┘
pid ┴ └───────────────┘
st ───┘└───────────────────────┘└─
42 rcases decidable.lt_trichotomy m n with h₃|h₃|h₃,
id └─────────────────────┘ ┴ ┴
src └─────┘└─────────────────────┘┴ ┴ └────────────┘
typ └─────┘└─────────────────────┘┴┴┴┴└────────────┘
doc └─────┘ ┴ ┴ └────────────┘
txt └─────┘ ┴ ┴ └────────────┘
par └─────┘ ┴ ┴ └────────────┘
pid ┴ ┴ ┴ └────────────┘
st ───────────────────────────────────────────────────┘└─
43 { exact h₂ _ h₃ },
id └┘ └┘
src └────┘ └─┘ ┴
typ └────┘└┘└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────┘└────────────┘└┘└
44 { rw h₃, exact h₁.fst },
id └┘ └────┘
src └─┘ └────┘└────┘┴
typ └─┘└┘ └────┘└────┘┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st ─────┘└───┘└─────────────┘└┘└
45 { injection mem_unique h₁ (al _ h₃) } },
id └────────┘ └┘ └┘ └┘
src └────────┘└────────┘┴ ┴ └─┘ └┘
typ └────────┘└────────┘┴└┘┴ └┘└─┘└┘└┘
doc └────────┘ ┴ ┴ └─┘ └┘
txt └────────┘ ┴ ┴ └─┘ └┘
par └────────┘ ┴ ┴ └─┘ └┘
pid ┴ ┴ ┴ └─┘ ┴┴
st ───────────────────────────────────────┘└──┘└
46 cases e : (p m).get pm,
id ┴ ┴ └┘
src └────┘ └─┘ ┴ └────┘
typ └────┘ └─┘ ┴┴┴└────┘└┘
doc └────┘ └─┘ ┴ └────┘
txt └────┘ └─┘ ┴ └────┘
par └────┘ └─┘ ┴ └────┘
pid ┴ └─┘ ┴ └────┘
st ───────────────────────┘└─
47 { suffices,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
48 exact IH _ ⟨rfl, this⟩ (λ n h, this _ (le_of_lt_succ h)),
id └┘ └─┘ └──┘ └───────────┘
src └────┘ └─┘ └─┘└┘ └┘ └────┘ └─┘ └───────────┘┴ └┘
typ └────┘└┘└─┘ └─┘└┘ └┘ └────┘└──┘└─┘ └───────────┘┴ └┘
doc └────┘ └─┘ └┘ └┘ └────┘ └─┘ ┴ └┘
txt └────┘ └─┘ └┘ └┘ └────┘ └─┘ ┴ └┘
par └────┘ └─┘ └┘ └┘ └────┘ └─┘ ┴ └┘
pid ┴ └─┘ └┘ └┘ └────┘ └─┘ ┴ └┘
st ───────────────────────────────────────────────────────────┘└─
49 intros n h, cases decidable.lt_or_eq_of_le h with h h,
id └──────────────────────┘ ┴
src └────────┘ └────┘└──────────────────────┘┴ └───────┘
typ └────────┘ └────┘└──────────────────────┘┴┴└───────┘
doc └────────┘ └────┘ ┴ └───────┘
txt └────────┘ └────┘ ┴ └───────┘
par └────────┘ └────┘ ┴ └───────┘
pid └──┘ ┴ ┴ └───────┘
st ─────────────┘└─────────────────────────────────────────┘└─
50 { exact al _ h },
id └┘ ┴
src └────┘ └─┘ ┴
typ └────┘└┘└─┘┴┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────┘└───────────┘└┘└
51 { rw h, exact ⟨_, e⟩ } },
id ┴ ┴
src └─┘ └────┘ └─┘ └┘
typ └─┘┴ └────┘ └─┘┴└┘
doc └─┘ └────┘ └─┘ └┘
txt └─┘ └────┘ └─┘ └┘
par └─┘ └────┘ └─┘ └┘
pid ┴ ┴ └─┘ ┴┴
st ─────────┘└─────────────┘└──┘└
52 { exact ⟨m, ⟨_, e⟩, al⟩ }
id ┴ ┴ └┘
src └────┘ └┘ └─┘ └─┘ └┘
typ └────┘ ┴└┘ └─┘┴└─┘└┘└┘
doc └────┘ └┘ └─┘ └─┘ └┘
txt └────┘ └┘ └─┘ └─┘ └┘
par └────┘ └┘ └─┘ └─┘ └┘
pid ┴ └┘ └─┘ └─┘ ┴┴
st ─────────────────────────┘└─
53 end
st ──┘
54
55 end rfind
56
57 def rfind (p : ℕ →. bool) : roption ℕ :=
id ┴ └┘ └──┘ └─────┘ ┴
src ┴ └┘ └──┘ └─────┘ ┴
typ ┴ └┘ └──┘ └─────┘ ┴
doc └┘ └─────┘
58 ⟨_, λ h, (rfind_x p h).1⟩
id ┴ └─────┘ ┴ ┴ ┴
src └─────┘ ┴
typ ┴ └─────┘ ┴ ┴ ┴
59
60 theorem rfind_spec {p : ℕ →. bool} {n : ℕ} (h : n ∈ rfind p) : tt ∈ p n :=
id ┴ └┘ └──┘ ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴
src ┴ └┘ └──┘ ┴ ┴ └───┘ └┘ ┴
typ ┴ └┘ └──┘ ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴
doc └┘
61 h.snd ▸ (rfind_x p h.fst).2.1
id ┴└──┘ ┴ └─────┘ ┴ ┴└──┘ ┴ ┴
src └──┘ ┴ └─────┘ └──┘ ┴ ┴
typ ┴└──┘ ┴ └─────┘ ┴ ┴└──┘ ┴ ┴
62
63 theorem rfind_min {p : ℕ →. bool} {n : ℕ} (h : n ∈ rfind p) :
id ┴ └┘ └──┘ ┴ ┴ ┴ └───┘ ┴
src ┴ └┘ └──┘ ┴ ┴ └───┘
typ ┴ └┘ └──┘ ┴ ┴ ┴ └───┘ ┴
doc └┘
64 ∀ {m : ℕ}, m < n → ff ∈ p m :=
id ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
65 h.snd ▸ (rfind_x p h.fst).2.2
id ┴└──┘ ┴ └─────┘ ┴ ┴└──┘ ┴ ┴
src └──┘ ┴ └─────┘ └──┘ ┴ ┴
typ ┴└──┘ ┴ └─────┘ ┴ ┴└──┘ ┴ ┴
66
67 @[simp] theorem rfind_dom {p : ℕ →. bool} :
id ┴ └┘ └──┘
src ┴ └┘ └──┘
typ ┴ └┘ └──┘
doc └──┘ └┘
68 (rfind p).dom ↔ ∃ n, tt ∈ p n ∧ ∀ {m : ℕ}, m < n → (p m).dom :=
id └───┘ ┴ └─┘ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └───┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
typ └───┘ ┴ └─┘ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
69 iff.rfl
id └─────┘
src └─────┘
typ └─────┘
70
71 @[simp] theorem rfind_dom' {p : ℕ →. bool} :
id ┴ └┘ └──┘
src ┴ └┘ └──┘
typ ┴ └┘ └──┘
doc └──┘ └┘
72 (rfind p).dom ↔ ∃ n, tt ∈ p n ∧ ∀ {m : ℕ}, m ≤ n → (p m).dom :=
id └───┘ ┴ └─┘ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └───┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
typ └───┘ ┴ └─┘ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
73 exists_congr $ λ n, and_congr_right $ λ pn,
id └──────────┘ ┴ └─────────────┘ └┘
src └──────────┘ └─────────────┘
typ └──────────┘ ┴ └─────────────┘ └┘
74 ⟨λ H m h, (eq_or_lt_of_le h).elim (λ e, e.symm ▸ pn.fst) (H _),
id ┴ ┴ ┴ └────────────┘ ┴ └──┘ ┴ ┴└───┘ ┴ └┘└──┘ ┴
src └────────────┘ └──┘ └───┘ ┴ └──┘
typ ┴ ┴ ┴ └────────────┘ ┴ └──┘ ┴ ┴└───┘ ┴ └┘└──┘ ┴
75 λ H m h, H (le_of_lt h)⟩
id ┴ ┴ ┴ ┴ └──────┘ ┴
src └──────┘
typ ┴ ┴ ┴ ┴ └──────┘ ┴
76
77 @[simp] theorem mem_rfind {p : ℕ →. bool} {n : ℕ} :
id ┴ └┘ └──┘ ┴
src ┴ └┘ └──┘ ┴
typ ┴ └┘ └──┘ ┴
doc └──┘ └┘
78 n ∈ rfind p ↔ tt ∈ p n ∧ ∀ {m : ℕ}, m < n → ff ∈ p m :=
id ┴ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
typ ┴ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
79 ⟨λ h, ⟨rfind_spec h, @rfind_min _ _ h⟩,
id ┴ └────────┘ ┴ └───────┘ ┴
src └────────┘ └───────┘
typ ┴ └────────┘ ┴ └───────┘ ┴
80 λ ⟨h₁, h₂⟩, let ⟨m, hm⟩ := dom_iff_mem.1 $
id ┴└┘ └┘ └─┘ └─────────┘┴
src └─────────┘┴
typ ┴└┘ └┘ └─┘ └─────────┘┴
81 (@rfind_dom p).2 ⟨_, h₁, λ m mn, (h₂ mn).fst⟩ in
id └───────┘ ┴ ┴ ┴ └┘ └┘ └─┘
src └───────┘ ┴ └─┘
typ └───────┘ ┴ ┴ ┴ └┘ └┘ └─┘
82 begin
st └─────
83 rcases lt_trichotomy m n with h|h|h,
id └───────────┘ ┴ ┴
src └─────┘└───────────┘┴ ┴ └─────────┘
typ └─────┘└───────────┘┴┴┴┴└─────────┘
doc └─────┘ ┴ ┴ └─────────┘
txt └─────┘ ┴ ┴ └─────────┘
par └─────┘ ┴ ┴ └─────────┘
pid ┴ ┴ ┴ └─────────┘
st ──────────────────────────────────────┘└─
84 { injection mem_unique (h₂ h) (rfind_spec hm) },
id └────────┘ └┘ ┴ └────────┘ └┘
src └────────┘└────────┘┴ ┴ └┘ └────────┘┴ └┘
typ └────────┘└────────┘┴ └┘┴┴└┘ └────────┘┴└┘└┘
doc └────────┘ ┴ ┴ └┘ ┴ └┘
txt └────────┘ ┴ ┴ └┘ ┴ └┘
par └────────┘ ┴ ┴ └┘ ┴ └┘
pid ┴ ┴ ┴ └┘ ┴ ┴┴
st ─────┘└──────────────────────────────────────────┘└┘└
85 { rwa ← h },
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid └─┘ ┴
st ─────┘└──────┘└┘└
86 { injection mem_unique h₁ (rfind_min hm h) },
id └────────┘ └┘ └───────┘ └┘ ┴
src └────────┘└────────┘┴ ┴ └───────┘┴ ┴ └┘
typ └────────┘└────────┘┴└┘┴ └───────┘┴└┘┴┴└┘
doc └────────┘ ┴ ┴ ┴ ┴ └┘
txt └────────┘ ┴ ┴ ┴ ┴ └┘
par └────────┘ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴┴
st ──────────────────────────────────────────────┘└──
87 end⟩
st ────┘
88
89 theorem rfind_min' {p : ℕ → bool} {m : ℕ} (pm : p m) :
id ┴ └──┘ ┴ ┴ ┴
src ┴ └──┘ ┴
typ ┴ └──┘ ┴ ┴ ┴
90 ∃ n ∈ rfind p, n ≤ m :=
id ┴ ┴ └───┘ ┴┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴
typ ┴ ┴ └───┘ ┴┴ ┴ ┴ ┴
91 have tt ∈ (p : ℕ →. bool) m, from ⟨trivial, pm⟩,
id └┘ ┴ ┴ ┴ └┘ └──┘ ┴ └─────┘ └┘
src └┘ ┴ ┴ └┘ └──┘ └─────┘
typ └┘ ┴ ┴ ┴ └┘ └──┘ ┴ └─────┘ └┘
doc └┘
92 let ⟨n, hn⟩ := dom_iff_mem.1 $
id └─┘ ┴ └┘ └─────────┘┴
src └─────────┘┴
typ └─┘ ┴ └┘ └─────────┘┴
93 (@rfind_dom p).2 ⟨m, this, λ k h, ⟨⟩⟩ in
id └───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └───────┘ ┴ ┴
typ └───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
94 ⟨n, hn, not_lt.1 $ λ h,
id └────┘┴ ┴
src └────┘┴
typ └────┘┴ ┴
95 by injection mem_unique this (rfind_min hn h)⟩
id └────────┘ └──┘ └───────┘ └┘ ┴
src └────────┘└────────┘┴ ┴ └───────┘┴ ┴ ┴
typ └────────┘└────────┘┴└──┘┴ └───────┘┴└┘┴┴┴
doc └────────┘ ┴ ┴ ┴ ┴ ┴
txt └────────┘ ┴ ┴ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st └─────────────────────────────────────────┘
96
97 theorem rfind_zero_none
98 (p : ℕ →. bool) (p0 : p 0 = none) : rfind p = none :=
id ┴ └┘ └──┘ ┴ ┴ └──┘ └───┘ ┴ ┴ └──┘
src ┴ └┘ └──┘ ┴ └──┘ └───┘ ┴ └──┘
typ ┴ └┘ └──┘ ┴ ┴ └──┘ └───┘ ┴ ┴ └──┘
doc └┘ └──┘ └──┘
99 eq_none_iff.2 $ λ a h,
id └─────────┘┴ ┴ ┴
src └─────────┘┴
typ └─────────┘┴ ┴ ┴
100 let ⟨n, h₁, h₂⟩ := rfind_dom'.1 h.fst in
id └─┘ └┘ └────────┘┴ ┴└──┘
src └────────┘┴ └──┘
typ └─┘ └┘ └────────┘┴ ┴└──┘
101 (p0 ▸ h₂ (zero_le _) : (@roption.none bool).dom)
id └┘ ┴ └─────┘ └──────────┘ └──┘ └─┘
src ┴ └─────┘ └──────────┘ └──┘ └─┘
typ └┘ ┴ └─────┘ └──────────┘ └──┘ └─┘
doc └──────────┘
102
103 def rfind_opt {α} (f : ℕ → option α) : roption α :=
id ┴ └────┘ ┴ └─────┘ ┴
src ┴ └────┘ └─────┘
typ ┴ └────┘ ┴ └─────┘ ┴
doc └─────┘
104 (rfind (λ n, (f n).is_some)).bind (λ n, f n)
id └───┘ ┴ ┴ ┴ └─────┘ └──┘ ┴ ┴ ┴
src └───┘ └─────┘ └──┘
typ └───┘ ┴ ┴ ┴ └─────┘ └──┘ ┴ ┴ ┴
doc └──┘
105
106 theorem rfind_opt_spec {α} {f : ℕ → option α} {a}
id ┴ └────┘ ┴
src ┴ └────┘
typ ┴ └────┘ ┴
107 (h : a ∈ rfind_opt f) : ∃ n, a ∈ f n :=
id ┴ ┴ └───────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ └───────┘ ┴ ┴ ┴
typ ┴ ┴ └───────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
108 let ⟨n, h₁, h₂⟩ := mem_bind_iff.1 h in ⟨n, mem_coe.1 h₂⟩
id └─┘ ┴ └┘ └──────────┘┴ ┴ └─────┘┴
src └──────────┘┴ └─────┘┴
typ └─┘ ┴ └┘ └──────────┘┴ ┴ └─────┘┴
109
110 theorem rfind_opt_dom {α} {f : ℕ → option α} :
id ┴ └────┘ ┴
src ┴ └────┘
typ ┴ └────┘ ┴
111 (rfind_opt f).dom ↔ ∃ n a, a ∈ f n :=
id └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴ ┴ ┴
typ └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
112 ⟨λ h, (rfind_opt_spec ⟨h, rfl⟩).imp (λ n h, ⟨_, h⟩),
id ┴ └────────────┘ ┴ └─┘ └─┘ ┴ ┴ ┴
src └────────────┘ └─┘ └─┘
typ ┴ └────────────┘ ┴ └─┘ └─┘ ┴ ┴ ┴
113 λ h, begin
id ┴
typ ┴
st └─────
114 have h' : ∃ n, (f n).is_some :=
id ┴ ┴ ┴
src └────────┘┴└┘┴┴ ┴ └────────────
typ └────────┘┴└┘┴┴ ┴┴ └────────────
doc └────────┘ └┘ ┴ ┴ └────────────
txt └────────┘ └┘ ┴ ┴ └────────────
par └────────┘ └┘ ┴ ┴ └────────────
pid └─────┘└─┘ └┘ ┴ ┴ └──────┘└────
st ──────────────────────────────────
115 h.imp (λ n, option.is_some_iff_exists.2),
id └───┘ └───────────────────────┘
src ───┘└───┘┴ └──┘└───────────────────────┘└─┘
typ ───┘└───┘┴ └──┘└───────────────────────┘└─┘
doc ───┘ ┴ └──┘ └─┘
txt ───┘ ┴ └──┘ └─┘
par ───┘ ┴ └──┘ └─┘
pid ───┘ ┴ └──┘ └─┘
st ───────────────────────────────────────────┘└─
116 have s := nat.find_spec h',
id └───────────┘ └┘
src └────────┘└───────────┘┴
typ └────────┘└───────────┘┴└┘
doc └────────┘ ┴
txt └────────┘ ┴
par └────────┘ ┴
pid └────┘┴└─┘ ┴
st ───────────────────────────┘└─
117 have fd : (rfind (λ n, (f n).is_some)).dom :=
id └───┘ ┴
src └────────┘ └───┘┴ └──┘ ┴ └──────────────────
typ └────────┘ └───┘┴ └──┘ ┴┴ └──────────────────
doc └────────┘ ┴ └──┘ ┴ └──────────────────
txt └────────┘ ┴ └──┘ ┴ └──────────────────
par └────────┘ ┴ └──┘ ┴ └──────────────────
pid └─────┘└─┘ ┴ └──┘ ┴ └────────────┘└────
st ────────────────────────────────────────────────
118 ⟨nat.find h', by simpa using s.symm, λ _ _, trivial⟩,
id └──────┘ └┘ └────┘ └─────┘
src ───┘ └──────┘┴ └┘ ┴└──────────┘└────┘└┘ └────┘└─────┘┴
typ ───┘ └──────┘┴└┘└┘ ┴└──────────┘└────┘└┘ └────┘└─────┘┴
doc ───┘ ┴ └┘ ┴└──────────┘ └┘ └────┘ ┴
txt ───┘ ┴ └┘ ┴└──────────┘ └┘ └────┘ ┴
par ───┘ ┴ └┘ ┴└──────────┘ └┘ └────┘ ┴
pid ───┘ ┴ └┘ └───────────┘ └┘ └────┘ ┴
st ───────────────────┘└─────────────────┘└───────────────┘└─
119 refine ⟨fd, _⟩,
id └┘
src └─────┘ └──┘
typ └─────┘ └┘└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ───────────────┘└─
120 have := rfind_spec (get_mem fd),
id └────────┘ └─────┘ └┘
src └──────┘└────────┘┴ └─────┘┴ ┴
typ └──────┘└────────┘┴ └─────┘┴└┘┴
doc └──────┘ ┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴
pid └───┘└─┘ ┴ ┴ ┴
st ────────────────────────────────┘└─
121 simp at this ⊢,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴└───────┘
st ───────────────┘└─
122 cases option.is_some_iff_exists.1 this.symm with a e,
id └───────────────────────┘ └───────┘
src └────┘└───────────────────────┘└─┘└───────┘└───────┘
typ └────┘└───────────────────────┘└─┘└───────┘└───────┘
doc └────┘ └─┘ └───────┘
txt └────┘ └─┘ └───────┘
par └────┘ └─┘ └───────┘
pid ┴ └─┘ └───────┘
st ─────────────────────────────────────────────────────┘└─
123 rw e, trivial
id ┴
src └─┘ └──────┘
typ └─┘┴ └──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ ┴
st ─────┘└────────┘
124 end⟩
st └─┘
125
126 theorem rfind_opt_mono {α} {f : ℕ → option α}
id ┴ └────┘ ┴
src ┴ └────┘
typ ┴ └────┘ ┴
127 (H : ∀ {a m n}, m ≤ n → a ∈ f m → a ∈ f n)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
128 {a} : a ∈ rfind_opt f ↔ ∃ n, a ∈ f n :=
id ┴ ┴ └───────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ └───────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
129 ⟨rfind_opt_spec, λ ⟨n, h⟩, begin
id └────────────┘ ┴
src └────────────┘
typ └────────────┘ ┴
st └─────
130 have h' := rfind_opt_dom.2 ⟨_, _, h⟩,
id └───────────┘ ┴
src └─────────┘└───────────┘└─┘ └────┘ ┴
typ └─────────┘└───────────┘└─┘ └────┘┴┴
doc └─────────┘ └─┘ └────┘ ┴
txt └─────────┘ └─┘ └────┘ ┴
par └─────────┘ └─┘ └────┘ ┴
pid └─────┘┴└─┘ └─┘ └────┘ ┴
st ─────────────────────────────────────┘└─
131 cases rfind_opt_spec ⟨h', rfl⟩ with k hk,
id └────────────┘ └┘ └─┘
src └────┘└────────────┘┴ └┘└─┘└─────────┘
typ └────┘└────────────┘┴ └┘└┘└─┘└─────────┘
doc └────┘ ┴ └┘ └─────────┘
txt └────┘ ┴ └┘ └─────────┘
par └────┘ ┴ └┘ └─────────┘
pid ┴ ┴ └┘ ┴└────────┘
st ─────────────────────────────────────────┘└─
132 have := (H (le_max_left _ _) h).symm.trans
id └─────────┘ ┴
src └──────┘ ┴ └─────────┘└────┘ └────────────
typ └──────┘ ┴ └─────────┘└────┘┴└────────────
doc └──────┘ ┴ └────┘ └────────────
txt └──────┘ ┴ └────┘ └────────────
par └──────┘ ┴ └────┘ └────────────
pid └───┘└─┘ ┴ └────┘ └────────────
st ─────────────────────────────────────────────
133 (H (le_max_right _ _) hk),
id ┴ └──────────┘ └┘
src ─────────┘ ┴ └──────────┘└────┘ ┴
typ ─────────┘ ┴┴ └──────────┘└────┘└┘┴
doc ─────────┘ ┴ └────┘ ┴
txt ─────────┘ ┴ └────┘ ┴
par ─────────┘ ┴ └────┘ ┴
pid ─────────┘ ┴ └────┘ ┴
st ──────────────────────────────────┘└─
134 simp at this, simp [this, get_mem]
id └──┘ └─────┘
src └──────────┘ └────┘ └┘└─────┘└┘
typ └──────────┘ └────┘└──┘└┘└─────┘└┘
doc └──────────┘ └────┘ └┘ └┘
txt └──────────┘ └────┘ └┘ └┘
par └──────────┘ └────┘ └┘ └┘
pid ┴└─────┘ ┴┴ └┘ ┴┴
st ─────────────┘└─────────────────────┘
135 end⟩
st └─┘
136
137 inductive partrec : (ℕ →. ℕ) → Prop
id ┴ └┘ ┴
src ┴ └┘ ┴
typ ┴ └┘ ┴
doc └┘
138 | zero : partrec (pure 0)
id └──┘
src └──┘
typ └──┘
139 | succ : partrec succ
id └──┘
src └──┘
typ └──┘
140 | left : partrec (λ n, n.unpair.1)
id ┴ ┴└─────┘┴
src └─────┘┴
typ ┴ ┴└─────┘┴
doc └─────┘
141 | right : partrec (λ n, n.unpair.2)
id ┴ ┴└─────┘┴
src └─────┘┴
typ ┴ ┴└─────┘┴
doc └─────┘
142 | pair {f g} : partrec f → partrec g → partrec (λ n, mkpair <$> f n <*> g n)
id ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ └────┘ └─┘ ┴ ┴ └─┘ ┴ ┴
src └────┘ └─┘ └─┘
typ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ └────┘ └─┘ ┴ ┴ └─┘ ┴ ┴
doc └────┘
143 | comp {f g} : partrec f → partrec g → partrec (λ n, g n >>= f)
id ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴
144 | prec {f g} : partrec f → partrec g → partrec (unpaired (λ a n,
id ┴ ┴ └─────┘ ┴ └─────┘ ┴ └──────┘ ┴ ┴
src └──────┘
typ ┴ ┴ └─────┘ ┴ └─────┘ ┴ └──────┘ ┴ ┴
145 n.elim (f a) (λ y IH, do i ← IH, g (mkpair a (mkpair y i)))))
id ┴└───┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └────┘ ┴ └────┘ ┴ ┴
src └───┘ └────┘ └────┘
typ ┴└───┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └────┘ ┴ └────┘ ┴ ┴
doc └────┘ └────┘
146 | rfind {f} : partrec f → partrec (λ a,
id ┴ └─────┘ ┴ ┴
typ ┴ └─────┘ ┴ ┴
147 rfind (λ n, (λ m, m = 0) <$> f (mkpair a n)))
id └───┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────┘ ┴ ┴
src └───┘ ┴ └─┘ └────┘
typ └───┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────┘ ┴ ┴
doc └────┘
148
149 namespace partrec
150
151 theorem of_eq {f g : ℕ →. ℕ} (hf : partrec f) (H : ∀ n, f n = g n) : partrec g :=
id ┴ └┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ └┘ ┴ └─────┘ ┴ └─────┘
typ ┴ └┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └┘
152 (funext H : f = g) ▸ hf
id └────┘ ┴ ┴ ┴ ┴ ┴ └┘
src └────┘ ┴ ┴
typ └────┘ ┴ ┴ ┴ ┴ ┴ └┘
153
154 theorem of_eq_tot {f : ℕ →. ℕ} {g : ℕ → ℕ}
id ┴ └┘ ┴ ┴ ┴
src ┴ └┘ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴
doc └┘
155 (hf : partrec f) (H : ∀ n, g n ∈ f n) : partrec g :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src └─────┘ ┴ └─────┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
156 hf.of_eq (λ n, eq_some_iff.2 (H n))
id └┘└────┘ ┴ └─────────┘┴ ┴ ┴
src └────┘ └─────────┘┴
typ └┘└────┘ ┴ └─────────┘┴ ┴ ┴
157
158 theorem of_primrec {f : ℕ → ℕ} (hf : primrec f) : partrec f :=
id ┴ ┴ └─────┘ ┴ └─────┘ ┴
src ┴ ┴ └─────┘ └─────┘
typ ┴ ┴ └─────┘ ┴ └─────┘ ┴
doc └─────┘
159 begin
st └─────
160 induction hf,
id └┘
src └────────┘
typ └────────┘└┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ─────────────┘└─
161 case nat.primrec.zero { exact zero },
id └──┘
src └──────────────────────┘└────┘└──┘┴┴
typ └──────────────────────┘└────┘└──┘┴┴
doc └──────────────────────┘└────┘ ┴┴
txt └──────────────────────┘└────┘ ┴┴
par └──────────────────────┘└────┘ ┴┴
pid └───────────────┘┴└──────┘ └┘
st ────────────────────────┘└──────────┘└┘└
162 case nat.primrec.succ { exact succ },
id └──┘
src └──────────────────────┘└────┘└──┘┴┴
typ └──────────────────────┘└────┘└──┘┴┴
doc └──────────────────────┘└────┘ ┴┴
txt └──────────────────────┘└────┘ ┴┴
par └──────────────────────┘└────┘ ┴┴
pid └───────────────┘┴└──────┘ └┘
st ────────────────────────┘└──────────┘└┘└
163 case nat.primrec.left { exact left },
id └──┘
src └──────────────────────┘└────┘└──┘┴┴
typ └──────────────────────┘└────┘└──┘┴┴
doc └──────────────────────┘└────┘ ┴┴
txt └──────────────────────┘└────┘ ┴┴
par └──────────────────────┘└────┘ ┴┴
pid └───────────────┘┴└──────┘ └┘
st ────────────────────────┘└──────────┘└┘└
164 case nat.primrec.right { exact right },
id └───┘
src └───────────────────────┘└────┘└───┘┴┴
typ └───────────────────────┘└────┘└───┘┴┴
doc └───────────────────────┘└────┘ ┴┴
txt └───────────────────────┘└────┘ ┴┴
par └───────────────────────┘└────┘ ┴┴
pid └────────────────┘┴└──────┘ └┘
st ─────────────────────────┘└───────────┘└┘└
165 case nat.primrec.pair : f g hf hg pf pg {
src └─────────────────────────────────────────
typ └─────────────────────────────────────────
doc └─────────────────────────────────────────
txt └─────────────────────────────────────────
par └─────────────────────────────────────────
pid └───────────────┘└────────────────┘└──
st ──────────────────────────────────────────┘└
166 refine (pf.pair pg).of_eq_tot (λ n, _),
id └─────┘ └┘
src ───┘└─────┘ └─────┘┴ └──────────┘ └────┘└─
typ ───┘└─────┘ └─────┘┴└┘└──────────┘ └────┘└─
doc ───┘└─────┘ ┴ └──────────┘ └────┘└─
txt ───┘└─────┘ ┴ └──────────┘ └────┘└─
par ───┘└─────┘ ┴ └──────────┘ └────┘└─
pid ──────────┘ ┴ └──────────┘ └───────
st ─────────────────────────────────────────┘└─
167 simp [has_seq.seq] },
src ───┘└────┘ └┘┴
typ ───┘└────┘ └┘┴
doc ───┘└────┘ └┘┴
txt ───┘└────┘ └┘┴
par ───┘└────┘ └┘┴
pid ─────────┘ └─┘
st ──────────────────────┘└┘└
168 case nat.primrec.comp : f g hf hg pf pg {
src └─────────────────────────────────────────
typ └─────────────────────────────────────────
doc └─────────────────────────────────────────
txt └─────────────────────────────────────────
par └─────────────────────────────────────────
pid └───────────────┘└────────────────┘└──
st ──────────────────────────────────────────┘└
169 refine (pf.comp pg).of_eq_tot (λ n, _),
id └─────┘ └┘
src ───┘└─────┘ └─────┘┴ └──────────┘ └────┘└─
typ ───┘└─────┘ └─────┘┴└┘└──────────┘ └────┘└─
doc ───┘└─────┘ ┴ └──────────┘ └────┘└─
txt ───┘└─────┘ ┴ └──────────┘ └────┘└─
par ───┘└─────┘ ┴ └──────────┘ └────┘└─
pid ──────────┘ ┴ └──────────┘ └───────
st ─────────────────────────────────────────┘└─
170 simp },
src ───┘└───┘┴
typ ───┘└───┘┴
doc ───┘└───┘┴
txt ───┘└───┘┴
par ───┘└───┘┴
pid ─────────┘
st ────────┘└┘└
171 case nat.primrec.prec : f g hf hg pf pg {
src └─────────────────────────────────────────
typ └─────────────────────────────────────────
doc └─────────────────────────────────────────
txt └─────────────────────────────────────────
par └─────────────────────────────────────────
pid └───────────────┘└────────────────┘└──
st ──────────────────────────────────────────┘└
172 refine (pf.prec pg).of_eq_tot (λ n, _),
id └─────┘ └┘
src ───┘└─────┘ └─────┘┴ └──────────┘ └────┘└─
typ ───┘└─────┘ └─────┘┴└┘└──────────┘ └────┘└─
doc ───┘└─────┘ ┴ └──────────┘ └────┘└─
txt ───┘└─────┘ ┴ └──────────┘ └────┘└─
par ───┘└─────┘ ┴ └──────────┘ └────┘└─
pid ──────────┘ ┴ └──────────┘ └───────
st ─────────────────────────────────────────┘└─
173 simp,
src ───┘└──┘└─
typ ───┘└──┘└─
doc ───┘└──┘└─
txt ───┘└──┘└─
par ───┘└──┘└─
pid ──────────
st ───────┘└─
174 induction n.unpair.2 with m IH, {simp},
id └──────┘
src ───┘└────────┘└──────┘└──────────┘└─┘└──┘└──
typ ───┘└────────┘└──────┘└──────────┘└─┘└──┘└──
doc ───┘└────────┘└──────┘└──────────┘└─┘└──┘└──
txt ───┘└────────┘ └──────────┘└─┘└──┘└──
par ───┘└────────┘ └──────────┘└─┘└──┘└──
pid ─────────────┘ └─────────────────────
st ─────────────────────────────────┘└─────┘┴└─
175 simp, exact ⟨_, IH, rfl⟩ },
id └┘ └─┘
src ───┘└──┘└┘└────┘ └─┘ └┘└─┘└┘┴
typ ───┘└──┘└┘└────┘ └─┘└┘└┘└─┘└┘┴
doc ───┘└──┘└┘└────┘ └─┘ └┘ └┘┴
txt ───┘└──┘└┘└────┘ └─┘ └┘ └┘┴
par ───┘└──┘└┘└────┘ └─┘ └┘ └┘┴
pid ───────────────┘ └─┘ └┘ └─┘
st ───────┘└───────────────────┘└──
176 end
st ──┘
177
178 protected theorem some : partrec some := of_primrec primrec.id
id └─────┘ └──┘ └────────┘ └────────┘
src └─────┘ └──┘ └────────┘ └────────┘
typ └─────┘ └──┘ └────────┘ └────────┘
doc └──┘
179
180 theorem none : partrec (λ n, none) :=
id └─────┘ ┴ └──┘
src └─────┘ └──┘
typ └─────┘ ┴ └──┘
doc └──┘
181 (of_primrec (nat.primrec.const 1)).rfind.of_eq $
id └────────┘ └───────────────┘ └───┘ └───┘
src └────────┘ └───────────────┘ └───┘ └───┘
typ └────────┘ └───────────────┘ └───┘ └───┘
182 λ n, eq_none_iff.2 $ λ a ⟨h, e⟩, by simpa using h
id ┴ └─────────┘┴ ┴ ┴ ┴
src └─────────┘┴ └──────────┘ └
typ ┴ └─────────┘┴ ┴ ┴ └──────────┘┴└
doc └──────────┘ └
txt └──────────┘ └
par └──────────┘ └
pid ┴└────┘ └
st └──────────────
183
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
184 theorem prec' {f g h}
185 (hf : partrec f) (hg : partrec g) (hh : partrec h) :
id └─────┘ ┴ └─────┘ ┴ └─────┘ ┴
src └─────┘ └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴
186 partrec (λ a, (f a).bind (λ n, n.elim (g a)
id └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴└───┘ ┴ ┴
src └─────┘ └──┘ └───┘
typ └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴└───┘ ┴ ┴
doc └──┘
187 (λ y IH, do i ← IH, h (mkpair a (mkpair y i))))) :=
id ┴ └┘ ┴ └┘ ┴ └────┘ ┴ └────┘ ┴ ┴
src └────┘ └────┘
typ ┴ └┘ ┴ └┘ ┴ └────┘ ┴ └────┘ ┴ ┴
doc └────┘ └────┘
188 ((prec hg hh).comp (pair partrec.some hf)).of_eq $
id └──┘ └┘ └┘ └──┘ └──┘ └──────────┘ └┘ └───┘
src └──┘ └──┘ └──┘ └──────────┘ └───┘
typ └──┘ └┘ └┘ └──┘ └──┘ └──────────┘ └┘ └───┘
189 λ a, ext $ λ s, by simp [(<*>)]; exact
id ┴ └─┘ ┴
src └─┘ └────┘ └───┘ └────┘
typ ┴ └─┘ ┴ └────┘ └───┘ └────┘
doc └─┘ └────┘ └───┘ └────┘
txt └────┘ └───┘ └────┘
par └────┘ └───┘ └────┘
pid ┴┴ └───┘ ┴
st └────────────────────
190 ⟨λ ⟨n, h₁, h₂⟩, ⟨_, ⟨_, h₁, rfl⟩, by simpa using h₂⟩,
src └┘ └┘ └┘ └─┘ └─┘ └─┘ └┘ └─┘ ┴└──────────┘ └──
typ └┘ └┘ └┘ └─┘ └─┘ └─┘ └┘ └─┘ ┴└──────────┘ └──
doc └┘ └┘ └┘ └─┘ └─┘ └─┘ └┘ └─┘ ┴└──────────┘ └──
txt └┘ └┘ └┘ └─┘ └─┘ └─┘ └┘ └─┘ ┴└──────────┘ └──
par └┘ └┘ └┘ └─┘ └─┘ └─┘ └┘ └─┘ ┴└──────────┘ └──
pid └┘ └┘ └┘ └─┘ └─┘ └─┘ └┘ └─┘ └───────────┘ └──
st ───────────────────────────────────┘ └──
191 λ ⟨_, ⟨n, h₁, rfl⟩, h₂⟩, ⟨_, h₁, by simpa using h₂⟩⟩
src ┘ └───┘ └┘ └┘ └─┘ └─┘ └─┘ └┘ ┴└──────────┘ └──
typ ┘ └───┘ └┘ └┘ └─┘ └─┘ └─┘ └┘ ┴└──────────┘ └──
doc ┘ └───┘ └┘ └┘ └─┘ └─┘ └─┘ └┘ ┴└──────────┘ └──
txt ┘ └───┘ └┘ └┘ └─┘ └─┘ └─┘ └┘ ┴└──────────┘ └──
par ┘ └───┘ └┘ └┘ └─┘ └─┘ └─┘ └┘ ┴└──────────┘ └──
pid ┘ └───┘ └┘ └┘ └─┘ └─┘ └─┘ └┘ └───────────┘ └┘└
st ───────────────────────────────────┘ └──
192
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
193 theorem ppred : partrec (λ n, ppred n) :=
id └─────┘ ┴ └───┘ ┴
src └─────┘ └───┘
typ └─────┘ ┴ └───┘ ┴
doc └───┘
194 have primrec₂ (λ n m, if n = nat.succ m then 0 else 1),
id └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src └──────┘ ┴ └──────┘
typ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └──────┘
195 from (primrec.ite
id └─────────┘
src └─────────┘
typ └─────────┘
196 (@@primrec_rel.comp _ _ _ _ _ _ _ primrec.eq
id └──────────────┘ └────────┘
src └──────────────┘ └────────┘
typ └──────────────┘ └────────┘
197 primrec.fst
id └─────────┘
src └─────────┘
typ └─────────┘
198 (_root_.primrec.succ.comp primrec.snd))
id └─────────────────┘└───┘ └─────────┘
src └─────────────────┘└───┘ └─────────┘
typ └─────────────────┘└───┘ └─────────┘
199 (_root_.primrec.const 0) (_root_.primrec.const 1)).to₂,
id └──────────────────┘ └──────────────────┘ └─┘
src └──────────────────┘ └──────────────────┘ └─┘
typ └──────────────────┘ └──────────────────┘ └─┘
200 (of_primrec (primrec₂.unpaired'.2 this)).rfind.of_eq $
id └────────┘ └────────────────┘┴ └──┘ └───┘ └───┘
src └────────┘ └────────────────┘┴ └───┘ └───┘
typ └────────┘ └────────────────┘┴ └──┘ └───┘ └───┘
201 λ n, begin
id ┴
typ ┴
st └─────
202 cases n; simp,
id ┴
src └────┘ └──┘
typ └────┘┴ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st ──────────────┘└─
203 { exact eq_none_iff.2 (λ a ⟨⟨m, h, _⟩, _⟩,
id └─────────┘
src └────┘└─────────┘└─┘ └──┘ └┘ └─────────
typ └────┘└─────────┘└─┘ └──┘ └┘ └─────────
doc └────┘ └─┘ └──┘ └┘ └─────────
txt └────┘ └─┘ └──┘ └┘ └─────────
par └────┘ └─┘ └──┘ └┘ └─────────
pid ┴ └─┘ └──┘ └┘ └─────────
st ───┘└────────────────────────────────────────
204 by simpa [show 0 ≠ m.succ, by intro h; injection h] using h) },
id ┴ └────┘ ┴ ┴
src ─────┘ ┴└─────┘ └─┘┴┴└────┘└───┘└─────┘└┘└────────┘ └──────┘ └┘
typ ─────┘ ┴└─────┘ └─┘┴┴└────┘└───┘└─────┘└┘└────────┘┴└──────┘┴└┘
doc ─────┘ ┴└─────┘ └─┘ ┴ └───┘└─────┘└┘└────────┘ └──────┘ └┘
txt ─────┘ ┴└─────┘ └─┘ ┴ └───┘└─────┘└┘└────────┘ └──────┘ └┘
par ─────┘ ┴└─────┘ └─┘ ┴ └───┘└─────┘└┘└────────┘ └──────┘ └┘
pid ─────┘ └──────┘ └─┘ ┴ └──────────────────────┘ └──────┘ ┴┴
st ───────┘└─────────────────────────┘└───────────────────┘└───────┘└┘└┘└
205 { refine eq_some_iff.2 _,
id └─────────┘
src └─────┘└─────────┘└──┘
typ └─────┘└─────────┘└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ─────────────────────────┘└─
206 simp, intros m h, simp [ne_of_gt h] }
id └──────┘ ┴
src └──┘ └────────┘ └────┘└──────┘┴ └┘
typ └──┘ └────────┘ └────┘└──────┘┴┴└┘
doc └──┘ └────────┘ └────┘ ┴ └┘
txt └──┘ └────────┘ └────┘ ┴ └┘
par └──┘ └────────┘ └────┘ ┴ └┘
pid └──┘ ┴┴ ┴ ┴┴
st ───────┘└──────────┘└──────────────────┘└─
207 end
st ──┘
208
209 end partrec
210
211 end nat
212
213 def partrec {α σ} [primcodable α] [primcodable σ]
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
214 (f : α →. σ) := nat.partrec (λ n,
id ┴ └┘ ┴ └─────────┘ ┴
src └┘ └─────────┘
typ ┴ └┘ ┴ └─────────┘ ┴
doc └┘
215 roption.bind (decode α n) (λ a, (f a).map encode))
id └──────────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘
src └──────────┘ └────┘ └─┘ └────┘
typ └──────────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘
doc └──────────┘ └─┘
216
217 def partrec₂ {α β σ} [primcodable α] [primcodable β] [primcodable σ]
id └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘ └─────────┘
218 (f : α → β →. σ) := partrec (λ p : α × β, f p.1 p.2)
id ┴ ┴ └┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴
src └┘ └─────┘ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴
doc └┘
219
220 def computable {α σ} [primcodable α] [primcodable σ] (f : α → σ) := partrec (f : α →. σ)
id └─────────┘ ┴ └─────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └┘ ┴
src └─────────┘ └─────────┘ └─────┘ └┘
typ └─────────┘ ┴ └─────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └┘ ┴
doc └─────────┘ └─────────┘ └┘
221
222 def computable₂ {α β σ} [primcodable α] [primcodable β] [primcodable σ]
id └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘ └─────────┘
223 (f : α → β → σ) := computable (λ p : α × β, f p.1 p.2)
id ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴
src └────────┘ ┴ ┴ ┴
typ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴
224
225 theorem primrec.to_comp {α σ} [primcodable α] [primcodable σ]
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
226 {f : α → σ} (hf : primrec f) : computable f :=
id ┴ ┴ └─────┘ ┴ └────────┘ ┴
src └─────┘ └────────┘
typ ┴ ┴ └─────┘ ┴ └────────┘ ┴
doc └─────┘
227 (nat.partrec.ppred.comp (nat.partrec.of_primrec hf)).of_eq $
id └───────────────┘└───┘ └────────────────────┘ └┘ └───┘
src └───────────────┘└───┘ └────────────────────┘ └───┘
typ └───────────────┘└───┘ └────────────────────┘ └┘ └───┘
228 λ n, by simp; cases decode α n; simp
id ┴ └────┘ ┴ ┴
src └──┘ └────┘└────┘┴ ┴ └────
typ ┴ └──┘ └────┘└────┘┴┴┴┴ └────
doc └──┘ └────┘ ┴ ┴ └────
txt └──┘ └────┘ ┴ ┴ └────
par └──┘ └────┘ ┴ ┴ └────
pid ┴ ┴ ┴ └
st └─────────────────────────────
229
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
230 theorem primrec₂.to_comp {α β σ} [primcodable α] [primcodable β] [primcodable σ]
id └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘ └─────────┘
231 {f : α → β → σ} (hf : primrec₂ f) : computable₂ f := hf.to_comp
id ┴ ┴ ┴ └──────┘ ┴ └─────────┘ ┴ └┘└──────┘
src └──────┘ └─────────┘ └──────┘
typ ┴ ┴ ┴ └──────┘ ┴ └─────────┘ ┴ └┘└──────┘
doc └──────┘
232
233 theorem computable.part {α σ} [primcodable α] [primcodable σ]
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
234 {f : α → σ} (hf : computable f) : partrec (f : α →. σ) := hf
id ┴ ┴ └────────┘ ┴ └─────┘ ┴ ┴ └┘ ┴ └┘
src └────────┘ └─────┘ └┘
typ ┴ ┴ └────────┘ ┴ └─────┘ ┴ ┴ └┘ ┴ └┘
doc └┘
235
236 theorem computable₂.part {α β σ} [primcodable α] [primcodable β] [primcodable σ]
id └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘ └─────────┘
237 {f : α → β → σ} (hf : computable₂ f) : partrec₂ (λ a, (f a : β →. σ)) := hf
id ┴ ┴ ┴ └─────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘
src └─────────┘ └──────┘ └┘
typ ┴ ┴ ┴ └─────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘
doc └┘
238
239 namespace computable
240 variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
241 variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
id └─────────┘ └─────────┘ └─────────┘ └─────────┘
src └─────────┘ └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ └─────────┘ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘ └─────────┘ └─────────┘
242
243 theorem of_eq {f g : α → σ} (hf : computable f) (H : ∀ n, f n = g n) : computable g :=
id ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴
src └────────┘ ┴ └────────┘
typ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴
244 (funext H : f = g) ▸ hf
id └────┘ ┴ ┴ ┴ ┴ ┴ └┘
src └────┘ ┴ ┴
typ └────┘ ┴ ┴ ┴ ┴ ┴ └┘
245
246 theorem const (s : σ) : computable (λ a : α, s) :=
id ┴ └────────┘ ┴ ┴
src └────────┘
typ ┴ └────────┘ ┴ ┴
247 (primrec.const _).to_comp
id └───────────┘ └─────┘
src └───────────┘ └─────┘
typ └───────────┘ └─────┘
248
249 theorem of_option {f : α → option β}
id ┴ └────┘ ┴
src └────┘
typ ┴ └────┘ ┴
250 (hf : computable f) : partrec (λ a, (f a : roption β)) :=
id └────────┘ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴
src └────────┘ └─────┘ └─────┘
typ └────────┘ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
251 (nat.partrec.ppred.comp hf).of_eq $ λ n, begin
id └───────────────┘└───┘ └┘ └───┘ ┴
src └───────────────┘└───┘ └───┘
typ └───────────────┘└───┘ └┘ └───┘ ┴
st └─────
252 cases decode α n with a; simp,
id └────┘ ┴ ┴
src └────┘└────┘┴ ┴ └─────┘ └──┘
typ └────┘└────┘┴┴┴┴└─────┘ └──┘
doc └────┘ ┴ ┴ └─────┘ └──┘
txt └────┘ ┴ ┴ └─────┘ └──┘
par └────┘ ┴ ┴ └─────┘ └──┘
pid ┴ ┴ ┴ └─────┘
st ──────────────────────────────┘└─
253 cases f a with b; simp
id ┴ ┴
src └────┘ ┴ └─────┘ └───┘
typ └────┘┴┴┴└─────┘ └───┘
doc └────┘ ┴ └─────┘ └───┘
txt └────┘ ┴ └─────┘ └───┘
par └────┘ ┴ └─────┘ └───┘
pid ┴ ┴ └─────┘ ┴
st ────────────────────────┘
254 end
st └─┘
255
256 theorem to₂ {f : α × β → σ} (hf : computable f) : computable₂ (λ a b, f (a, b)) :=
id ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴┴ ┴
src ┴ └────────┘ └─────────┘ ┴
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴┴ ┴
257 hf.of_eq $ λ ⟨a, b⟩, rfl
id └┘└────┘ ┴ └─┘
src └────┘ └─┘
typ └┘└────┘ ┴ └─┘
258
259 protected theorem id : computable (@id α) := primrec.id.to_comp
id └────────┘ └┘ ┴ └────────┘└──────┘
src └────────┘ └┘ └────────┘└──────┘
typ └────────┘ └┘ ┴ └────────┘└──────┘
260
261 theorem fst : computable (@prod.fst α β) := primrec.fst.to_comp
id └────────┘ └──────┘ ┴ ┴ └─────────┘└──────┘
src └────────┘ └──────┘ └─────────┘└──────┘
typ └────────┘ └──────┘ ┴ ┴ └─────────┘└──────┘
262
263 theorem snd : computable (@prod.snd α β) := primrec.snd.to_comp
id └────────┘ └──────┘ ┴ ┴ └─────────┘└──────┘
src └────────┘ └──────┘ └─────────┘└──────┘
typ └────────┘ └──────┘ ┴ ┴ └─────────┘└──────┘
264
265 theorem pair {f : α → β} {g : α → γ}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
266 (hf : computable f) (hg : computable g) : computable (λ a, (f a, g a)) :=
id └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘ ┴
typ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴┴ ┴ ┴ ┴
267 (hf.pair hg).of_eq $
id └┘└───┘ └┘ └───┘
src └───┘ └───┘
typ └┘└───┘ └┘ └───┘
268 λ n, by cases decode α n; simp [(<*>)]
id ┴ └────┘ ┴ ┴
src └────┘└────┘┴ ┴ └────┘ └─────
typ ┴ └────┘└────┘┴┴┴┴ └────┘ └─────
doc └────┘ ┴ ┴ └────┘ └─────
txt └────┘ ┴ ┴ └────┘ └─────
par └────┘ ┴ ┴ └────┘ └─────
pid ┴ ┴ ┴ ┴┴ └───┘└
st └───────────────────────────────
269
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
270 theorem unpair : computable nat.unpair := primrec.unpair.to_comp
id └────────┘ └────────┘ └────────────┘└──────┘
src └────────┘ └────────┘ └────────────┘└──────┘
typ └────────┘ └────────┘ └────────────┘└──────┘
doc └────────┘
271
272 theorem succ : computable nat.succ := primrec.succ.to_comp
id └────────┘ └──────┘ └──────────┘└──────┘
src └────────┘ └──────┘ └──────────┘└──────┘
typ └────────┘ └──────┘ └──────────┘└──────┘
273 theorem pred : computable nat.pred := primrec.pred.to_comp
id └────────┘ └──────┘ └──────────┘└──────┘
src └────────┘ └──────┘ └──────────┘└──────┘
typ └────────┘ └──────┘ └──────────┘└──────┘
274 theorem nat_bodd : computable nat.bodd := primrec.nat_bodd.to_comp
id └────────┘ └──────┘ └──────────────┘└──────┘
src └────────┘ └──────┘ └──────────────┘└──────┘
typ └────────┘ └──────┘ └──────────────┘└──────┘
275 theorem nat_div2 : computable nat.div2 := primrec.nat_div2.to_comp
id └────────┘ └──────┘ └──────────────┘└──────┘
src └────────┘ └──────┘ └──────────────┘└──────┘
typ └────────┘ └──────┘ └──────────────┘└──────┘
276
277 theorem sum_inl : computable (@sum.inl α β) := primrec.sum_inl.to_comp
id └────────┘ └─────┘ ┴ ┴ └─────────────┘└──────┘
src └────────┘ └─────┘ └─────────────┘└──────┘
typ └────────┘ └─────┘ ┴ ┴ └─────────────┘└──────┘
278 theorem sum_inr : computable (@sum.inr α β) := primrec.sum_inr.to_comp
id └────────┘ └─────┘ ┴ ┴ └─────────────┘└──────┘
src └────────┘ └─────┘ └─────────────┘└──────┘
typ └────────┘ └─────┘ ┴ ┴ └─────────────┘└──────┘
279
280 theorem list_cons : computable₂ (@list.cons α) := primrec.list_cons.to_comp
id └─────────┘ └───────┘ ┴ └───────────────┘└──────┘
src └─────────┘ └───────┘ └───────────────┘└──────┘
typ └─────────┘ └───────┘ ┴ └───────────────┘└──────┘
281 theorem list_reverse : computable (@list.reverse α) := primrec.list_reverse.to_comp
id └────────┘ └──────────┘ ┴ └──────────────────┘└──────┘
src └────────┘ └──────────┘ └──────────────────┘└──────┘
typ └────────┘ └──────────┘ ┴ └──────────────────┘└──────┘
282 theorem list_nth : computable₂ (@list.nth α) := primrec.list_nth.to_comp
id └─────────┘ └──────┘ ┴ └──────────────┘└──────┘
src └─────────┘ └──────┘ └──────────────┘└──────┘
typ └─────────┘ └──────┘ ┴ └──────────────┘└──────┘
283 theorem list_append : computable₂ ((++) : list α → list α → list α) := primrec.list_append.to_comp
id └─────────┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └─────────────────┘└──────┘
src └─────────┘ ┴ └──┘ └──┘ └──┘ └─────────────────┘└──────┘
typ └─────────┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └─────────────────┘└──────┘
284 theorem list_concat : computable₂ (λ l (a:α), l ++ [a]) := primrec.list_concat.to_comp
id └─────────┘ ┴ ┴ ┴ └┘ ┴┴┴ └─────────────────┘└──────┘
src └─────────┘ └┘ ┴ ┴ └─────────────────┘└──────┘
typ └─────────┘ ┴ ┴ ┴ └┘ ┴┴┴ └─────────────────┘└──────┘
285 theorem list_length : computable (@list.length α) := primrec.list_length.to_comp
id └────────┘ └─────────┘ ┴ └─────────────────┘└──────┘
src └────────┘ └─────────┘ └─────────────────┘└──────┘
typ └────────┘ └─────────┘ ┴ └─────────────────┘└──────┘
286
287 theorem vector_cons {n} : computable₂ (@vector.cons α n) := primrec.vector_cons.to_comp
id └─────────┘ └─────────┘ ┴ ┴ └─────────────────┘└──────┘
src └─────────┘ └─────────┘ └─────────────────┘└──────┘
typ └─────────┘ └─────────┘ ┴ ┴ └─────────────────┘└──────┘
288 theorem vector_to_list {n} : computable (@vector.to_list α n) := primrec.vector_to_list.to_comp
id └────────┘ └────────────┘ ┴ ┴ └────────────────────┘└──────┘
src └────────┘ └────────────┘ └────────────────────┘└──────┘
typ └────────┘ └────────────┘ ┴ ┴ └────────────────────┘└──────┘
289 theorem vector_length {n} : computable (@vector.length α n) := primrec.vector_length.to_comp
id └────────┘ └───────────┘ ┴ ┴ └───────────────────┘└──────┘
src └────────┘ └───────────┘ └───────────────────┘└──────┘
typ └────────┘ └───────────┘ ┴ ┴ └───────────────────┘└──────┘
290 theorem vector_head {n} : computable (@vector.head α n) := primrec.vector_head.to_comp
id └────────┘ └─────────┘ ┴ ┴ └─────────────────┘└──────┘
src └────────┘ └─────────┘ └─────────────────┘└──────┘
typ └────────┘ └─────────┘ ┴ ┴ └─────────────────┘└──────┘
291 theorem vector_tail {n} : computable (@vector.tail α n) := primrec.vector_tail.to_comp
id └────────┘ └─────────┘ ┴ ┴ └─────────────────┘└──────┘
src └────────┘ └─────────┘ └─────────────────┘└──────┘
typ └────────┘ └─────────┘ ┴ ┴ └─────────────────┘└──────┘
292 theorem vector_nth {n} : computable₂ (@vector.nth α n) := primrec.vector_nth.to_comp
id └─────────┘ └────────┘ ┴ ┴ └────────────────┘└──────┘
src └─────────┘ └────────┘ └────────────────┘└──────┘
typ └─────────┘ └────────┘ ┴ ┴ └────────────────┘└──────┘
293 theorem vector_nth' {n} : computable (@vector.nth α n) := primrec.vector_nth'.to_comp
id └────────┘ └────────┘ ┴ ┴ └─────────────────┘└──────┘
src └────────┘ └────────┘ └─────────────────┘└──────┘
typ └────────┘ └────────┘ ┴ ┴ └─────────────────┘└──────┘
294 theorem vector_of_fn' {n} : computable (@vector.of_fn α n) := primrec.vector_of_fn'.to_comp
id └────────┘ └──────────┘ ┴ ┴ └───────────────────┘└──────┘
src └────────┘ └──────────┘ └───────────────────┘└──────┘
typ └────────┘ └──────────┘ ┴ ┴ └───────────────────┘└──────┘
295
296 theorem fin_app {n} : computable₂ (@id (fin n → σ)) := primrec.fin_app.to_comp
id └─────────┘ └┘ └─┘ ┴ ┴ └─────────────┘└──────┘
src └─────────┘ └┘ └─┘ └─────────────┘└──────┘
typ └─────────┘ └┘ └─┘ ┴ ┴ └─────────────┘└──────┘
297
298 protected theorem encode : computable (@encode α _) :=
id └────────┘ └────┘ ┴
src └────────┘ └────┘
typ └────────┘ └────┘ ┴
299 primrec.encode.to_comp
id └────────────┘└──────┘
src └────────────┘└──────┘
typ └────────────┘└──────┘
300
301 protected theorem decode : computable (decode α) :=
id └────────┘ └────┘ ┴
src └────────┘ └────┘
typ └────────┘ └────┘ ┴
302 primrec.decode.to_comp
id └────────────┘└──────┘
src └────────────┘└──────┘
typ └────────────┘└──────┘
303
304 protected theorem of_nat (α) [denumerable α] : computable (of_nat α) :=
id └─────────┘ ┴ └────────┘ └────┘ ┴
src └─────────┘ └────────┘ └────┘
typ └─────────┘ ┴ └────────┘ └────┘ ┴
doc └─────────┘
305 (primrec.of_nat _).to_comp
id └────────────┘ └─────┘
src └────────────┘ └─────┘
typ └────────────┘ └─────┘
306
307 theorem encode_iff {f : α → σ} : computable (λ a, encode (f a)) ↔ computable f :=
id ┴ ┴ └────────┘ ┴ └────┘ ┴ ┴ ┴ └────────┘ ┴
src └────────┘ └────┘ ┴ └────────┘
typ ┴ ┴ └────────┘ ┴ └────┘ ┴ ┴ ┴ └────────┘ ┴
308 iff.rfl
id └─────┘
src └─────┘
typ └─────┘
309
310 theorem option_some : computable (@option.some α) :=
id └────────┘ └─────────┘ ┴
src └────────┘ └─────────┘
typ └────────┘ └─────────┘ ┴
311 primrec.option_some.to_comp
id └─────────────────┘└──────┘
src └─────────────────┘└──────┘
typ └─────────────────┘└──────┘
312
313 end computable
314
315 namespace partrec
316 variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
317 variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
id └─────────┘ └─────────┘ └─────────┘ └─────────┘
src └─────────┘ └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ └─────────┘ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘ └─────────┘ └─────────┘
318
319 open computable
320
321 theorem of_eq {f g : α →. σ} (hf : partrec f) (H : ∀ n, f n = g n) : partrec g :=
id ┴ └┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src └┘ └─────┘ ┴ └─────┘
typ ┴ └┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └┘
322 (funext H : f = g) ▸ hf
id └────┘ ┴ ┴ ┴ ┴ ┴ └┘
src └────┘ ┴ ┴
typ └────┘ ┴ ┴ ┴ ┴ ┴ └┘
323
324 theorem of_eq_tot {f : α →. σ} {g : α → σ}
id ┴ └┘ ┴ ┴ ┴
src └┘
typ ┴ └┘ ┴ ┴ ┴
doc └┘
325 (hf : partrec f) (H : ∀ n, g n ∈ f n) : computable g :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴
src └─────┘ ┴ └────────┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴
326 hf.of_eq (λ a, eq_some_iff.2 (H a))
id └┘└────┘ ┴ └─────────┘┴ ┴ ┴
src └────┘ └─────────┘┴
typ └┘└────┘ ┴ └─────────┘┴ ┴ ┴
327
328 theorem none : partrec (λ a : α, @roption.none σ) :=
id └─────┘ ┴ └──────────┘ ┴
src └─────┘ └──────────┘
typ └─────┘ ┴ └──────────┘ ┴
doc └──────────┘
329 nat.partrec.none.of_eq $ λ n, by cases decode α n; simp
id └──────────────┘└────┘ ┴ └────┘ ┴ ┴
src └──────────────┘└────┘ └────┘└────┘┴ ┴ └────
typ └──────────────┘└────┘ ┴ └────┘└────┘┴┴┴┴ └────
doc └────┘ ┴ ┴ └────
txt └────┘ ┴ ┴ └────
par └────┘ ┴ ┴ └────
pid ┴ ┴ ┴ └
st └───────────────────────
330
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
331 protected theorem some : partrec (@roption.some α) := computable.id
id └─────┘ └──────────┘ ┴ └───────────┘
src └─────┘ └──────────┘ └───────────┘
typ └─────┘ └──────────┘ ┴ └───────────┘
doc └──────────┘
332
333 theorem const' (s : roption σ) : partrec (λ a : α, s) :=
id └─────┘ ┴ └─────┘ ┴ ┴
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ ┴
doc └─────┘
334 by haveI := classical.dec s.dom; exact
id └───────────┘ └───┘
src └───────┘└───────────┘┴└───┘ └────┘
typ └───────┘└───────────┘┴└───┘ └────┘
doc └───────┘ ┴ └────┘
txt └───────┘ ┴ └────┘
par └───────┘ ┴ └────┘
pid ┴└─┘ ┴ ┴
st └────────────────────────────────────
335 (of_option (const (to_option s))).of_eq (λ a, of_to_option s)
id └───────┘ └───┘ └───────┘ └──────────┘ ┴
src └───────┘┴ └───┘┴ └───────┘┴ └────────┘ └──┘└──────────┘┴ └─
typ └───────┘┴ └───┘┴ └───────┘┴ └────────┘ └──┘└──────────┘┴┴└─
doc ┴ ┴ └───────┘┴ └────────┘ └──┘ ┴ └─
txt ┴ ┴ ┴ └────────┘ └──┘ ┴ └─
par ┴ ┴ ┴ └────────┘ └──┘ ┴ └─
pid ┴ ┴ ┴ └────────┘ └──┘ ┴ ┴└
st ──────────────────────────────────────────────────────────────
336
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
337 protected theorem bind {f : α →. β} {g : α → β →. σ}
id ┴ └┘ ┴ ┴ ┴ └┘ ┴
src └┘ └┘
typ ┴ └┘ ┴ ┴ ┴ └┘ ┴
doc └┘ └┘
338 (hf : partrec f) (hg : partrec₂ g) : partrec (λ a, (f a).bind (g a)) :=
id └─────┘ ┴ └──────┘ ┴ └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴
src └─────┘ └──────┘ └─────┘ └──┘
typ └─────┘ ┴ └──────┘ ┴ └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴
doc └──┘
339 (hg.comp (nat.partrec.some.pair hf)).of_eq $
id └┘└───┘ └──────────────┘└───┘ └┘ └───┘
src └───┘ └──────────────┘└───┘ └───┘
typ └┘└───┘ └──────────────┘└───┘ └┘ └───┘
340 λ n, by simp [(<*>)]; cases e : decode α n with a;
id ┴ └────┘ ┴ ┴
src └────┘ └───┘ └────┘ └─┘└────┘┴ ┴ └─────┘
typ ┴ └────┘ └───┘ └────┘ └─┘└────┘┴┴┴┴└─────┘
doc └────┘ └───┘ └────┘ └─┘ ┴ ┴ └─────┘
txt └────┘ └───┘ └────┘ └─┘ ┴ ┴ └─────┘
par └────┘ └───┘ └────┘ └─┘ ┴ ┴ └─────┘
pid ┴┴ └───┘ ┴ └─┘ ┴ ┴ └─────┘
st └───────────────────────────────────────────
341 simp [e, encodek]
id ┴ └─────┘
src └────┘ └┘└─────┘└─
typ └────┘┴└┘└─────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st ────────────────────
342
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
343 theorem map {f : α →. β} {g : α → β → σ}
id ┴ └┘ ┴ ┴ ┴ ┴
src └┘
typ ┴ └┘ ┴ ┴ ┴ ┴
doc └┘
344 (hf : partrec f) (hg : computable₂ g) : partrec (λ a, (f a).map (g a)) :=
id └─────┘ ┴ └─────────┘ ┴ └─────┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └─────┘ └─────────┘ └─────┘ └─┘
typ └─────┘ ┴ └─────────┘ ┴ └─────┘ ┴ ┴ ┴ └─┘ ┴ ┴
doc └─┘
345 by simpa [bind_some_eq_map] using
id └──────────────┘
src └─────┘└──────────────┘└───────
typ └─────┘└──────────────┘└───────
doc └─────┘ └───────
txt └─────┘ └───────
par └─────┘ └───────
pid ┴┴ ┴┴└─────
st └───────────────────────────────
346 @@partrec.bind _ _ _ (λ a b, roption.some (g a b)) hf hg
id └──────────┘ └──────────┘ ┴ └┘ └┘
src ──┘ └──────────┘└─────┘ └────┘└──────────┘┴ ┴ ┴ └─┘ ┴ └
typ ──┘ └──────────┘└─────┘ └────┘└──────────┘┴ ┴┴ ┴ └─┘└┘┴└┘└
doc ──┘ └─────┘ └────┘└──────────┘┴ ┴ ┴ └─┘ ┴ └
txt ──┘ └─────┘ └────┘ ┴ ┴ ┴ └─┘ ┴ └
par ──┘ └─────┘ └────┘ ┴ ┴ ┴ └─┘ ┴ └
pid ──┘ └─────┘ └────┘ ┴ ┴ ┴ └─┘ ┴ └
st ────────────────────────────────────────────────────────────
347
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
348 theorem to₂ {f : α × β →. σ} (hf : partrec f) : partrec₂ (λ a b, f (a, b)) :=
id ┴ ┴ ┴ └┘ ┴ └─────┘ ┴ └──────┘ ┴ ┴ ┴ ┴┴ ┴
src ┴ └┘ └─────┘ └──────┘ ┴
typ ┴ ┴ ┴ └┘ ┴ └─────┘ ┴ └──────┘ ┴ ┴ ┴ ┴┴ ┴
doc └┘
349 hf.of_eq $ λ ⟨a, b⟩, rfl
id └┘└────┘ ┴ └─┘
src └────┘ └─┘
typ └┘└────┘ ┴ └─┘
350
351 theorem nat_elim
352 {f : α → ℕ} {g : α →. σ} {h : α → ℕ × σ →. σ}
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ └┘ ┴ ┴ └┘
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └┘ └┘
353 (hf : computable f) (hg : partrec g) (hh : partrec₂ h) :
id └────────┘ ┴ └─────┘ ┴ └──────┘ ┴
src └────────┘ └─────┘ └──────┘
typ └────────┘ ┴ └─────┘ ┴ └──────┘ ┴
354 partrec (λ a, (f a).elim (g a) (λ y IH, IH.bind (λ i, h a (y, i)))) :=
id └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ └┘└───┘ ┴ ┴ ┴ ┴┴ ┴
src └─────┘ └──┘ └───┘ ┴
typ └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ └┘└───┘ ┴ ┴ ┴ ┴┴ ┴
doc └───┘
355 (nat.partrec.prec' hf hg hh).of_eq $ λ n, begin
id └───────────────┘ └┘ └┘ └┘ └───┘ ┴
src └───────────────┘ └───┘
typ └───────────────┘ └┘ └┘ └┘ └───┘ ┴
st └─────
356 cases e : decode α n with a; simp [e],
id └────┘ ┴ ┴ ┴
src └────┘ └─┘└────┘┴ ┴ └─────┘ └────┘ ┴
typ └────┘ └─┘└────┘┴┴┴┴└─────┘ └────┘┴┴
doc └────┘ └─┘ ┴ ┴ └─────┘ └────┘ ┴
txt └────┘ └─┘ ┴ ┴ └─────┘ └────┘ ┴
par └────┘ └─┘ ┴ ┴ └─────┘ └────┘ ┴
pid ┴ └─┘ ┴ ┴ └─────┘ ┴┴ ┴
st ──────────────────────────────────────┘└─
357 induction f a with m IH; simp,
id ┴ ┴
src └────────┘ ┴ └────────┘ └──┘
typ └────────┘┴┴┴└────────┘ └──┘
doc └────────┘ ┴ └────────┘ └──┘
txt └────────┘ ┴ └────────┘ └──┘
par └────────┘ ┴ └────────┘ └──┘
pid ┴ ┴ ┴└───────┘
st ──────────────────────────────┘└─
358 rw [IH, bind_map],
id └┘ └──────┘
src └──┘ └┘└──────┘┴
typ └──┘└┘└┘└──────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────┘└────────┘┴└─
359 congr, funext s,
src └───┘ └──────┘
typ └───┘ └──────┘
doc └──────┘
txt └───┘ └──────┘
par └───┘ └──────┘
pid └┘
st ──────┘└────────┘└─
360 simp [encodek]
id └─────┘
src └────┘└─────┘└┘
typ └────┘└─────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ────────────────┘
361 end
st └─┘
362
363 theorem comp {f : β →. σ} {g : α → β}
id ┴ └┘ ┴ ┴ ┴
src └┘
typ ┴ └┘ ┴ ┴ ┴
doc └┘
364 (hf : partrec f) (hg : computable g) : partrec (λ a, f (g a)) :=
id └─────┘ ┴ └────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
src └─────┘ └────────┘ └─────┘
typ └─────┘ ┴ └────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
365 (hf.comp hg).of_eq $
id └┘└───┘ └┘ └───┘
src └───┘ └───┘
typ └┘└───┘ └┘ └───┘
366 λ n, by simp; cases e : decode α n with a;
id ┴ └────┘ ┴ ┴
src └──┘ └────┘ └─┘└────┘┴ ┴ └─────┘
typ ┴ └──┘ └────┘ └─┘└────┘┴┴┴┴└─────┘
doc └──┘ └────┘ └─┘ ┴ ┴ └─────┘
txt └──┘ └────┘ └─┘ ┴ ┴ └─────┘
par └──┘ └────┘ └─┘ ┴ ┴ └─────┘
pid ┴ └─┘ ┴ ┴ └─────┘
st └───────────────────────────────────
367 simp [e, encodek]
id ┴ └─────┘
src └────┘ └┘└─────┘└─
typ └────┘┴└┘└─────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st ────────────────────
368
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
369 theorem nat_iff {f : ℕ →. ℕ} : partrec f ↔ nat.partrec f :=
id ┴ └┘ ┴ └─────┘ ┴ ┴ └─────────┘ ┴
src ┴ └┘ ┴ └─────┘ ┴ └─────────┘
typ ┴ └┘ ┴ └─────┘ ┴ ┴ └─────────┘ ┴
doc └┘
370 by simp [partrec, map_id']
id └─────┘ └─────┘
src └────┘└─────┘└┘└─────┘└─
typ └────┘└─────┘└┘└─────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └────────────────────────
371
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
372 theorem map_encode_iff {f : α →. σ} : partrec (λ a, (f a).map encode) ↔ partrec f :=
id ┴ └┘ ┴ └─────┘ ┴ ┴ ┴ └─┘ └────┘ ┴ └─────┘ ┴
src └┘ └─────┘ └─┘ └────┘ ┴ └─────┘
typ ┴ └┘ ┴ └─────┘ ┴ ┴ ┴ └─┘ └────┘ ┴ └─────┘ ┴
doc └┘ └─┘
373 iff.rfl
id └─────┘
src └─────┘
typ └─────┘
374
375 end partrec
376
377 namespace partrec₂
378 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {σ : Type*}
379 variables [primcodable α] [primcodable β] [primcodable γ] [primcodable δ] [primcodable σ]
id └─────────┘ └─────────┘ └─────────┘ └─────────┘ └─────────┘
src └─────────┘ └─────────┘ └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ └─────────┘ └─────────┘ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘ └─────────┘ └─────────┘ └─────────┘
380
381 theorem unpaired {f : ℕ → ℕ →. α} : partrec (nat.unpaired f) ↔ partrec₂ f :=
id ┴ ┴ └┘ ┴ └─────┘ └──────────┘ ┴ ┴ └──────┘ ┴
src ┴ ┴ └┘ └─────┘ └──────────┘ ┴ └──────┘
typ ┴ ┴ └┘ ┴ └─────┘ └──────────┘ ┴ ┴ └──────┘ ┴
doc └┘
382 ⟨λ h, by simpa using h.comp primrec₂.mkpair.to_comp,
id ┴ └────┘ └─────────────────────┘
src └──────────┘└────┘┴└─────────────────────┘
typ ┴ └──────────┘└────┘┴└─────────────────────┘
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid ┴└────┘ ┴
st └─────────────────────────────────────────┘
383 λ h, h.comp primrec.unpair.to_comp⟩
id ┴ ┴└───┘ └────────────┘└──────┘
src └───┘ └────────────┘└──────┘
typ ┴ ┴└───┘ └────────────┘└──────┘
384
385 theorem unpaired' {f : ℕ → ℕ →. ℕ} : nat.partrec (nat.unpaired f) ↔ partrec₂ f :=
id ┴ ┴ └┘ ┴ └─────────┘ └──────────┘ ┴ ┴ └──────┘ ┴
src ┴ ┴ └┘ ┴ └─────────┘ └──────────┘ ┴ └──────┘
typ ┴ ┴ └┘ ┴ └─────────┘ └──────────┘ ┴ ┴ └──────┘ ┴
doc └┘
386 partrec.nat_iff.symm.trans unpaired
id └─────────────┘└───┘└────┘ └──────┘
src └─────────────┘└───┘└────┘ └──────┘
typ └─────────────┘└───┘└────┘ └──────┘
387
388 theorem comp
389 {f : β → γ →. σ} {g : α → β} {h : α → γ}
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └┘
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └┘
390 (hf : partrec₂ f) (hg : computable g) (hh : computable h) :
id └──────┘ ┴ └────────┘ ┴ └────────┘ ┴
src └──────┘ └────────┘ └────────┘
typ └──────┘ ┴ └────────┘ ┴ └────────┘ ┴
391 partrec (λ a, f (g a) (h a)) := hf.comp (hg.pair hh)
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ └┘└───┘ └┘
src └─────┘ └───┘ └───┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ └┘└───┘ └┘
392
393 theorem comp₂
394 {f : γ → δ →. σ} {g : α → β → γ} {h : α → β → δ}
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
395 (hf : partrec₂ f) (hg : computable₂ g) (hh : computable₂ h) :
id └──────┘ ┴ └─────────┘ ┴ └─────────┘ ┴
src └──────┘ └─────────┘ └─────────┘
typ └──────┘ ┴ └─────────┘ ┴ └─────────┘ ┴
396 partrec₂ (λ a b, f (g a b) (h a b)) := hf.comp hg hh
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ └┘ └┘
src └──────┘ └───┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ └┘ └┘
397
398 end partrec₂
399
400 namespace computable
401 variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
402 variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
id └─────────┘ └─────────┘ └─────────┘ └─────────┘
src └─────────┘ └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ └─────────┘ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘ └─────────┘ └─────────┘
403
404 theorem comp {f : β → σ} {g : α → β}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
405 (hf : computable f) (hg : computable g) :
id └────────┘ ┴ └────────┘ ┴
src └────────┘ └────────┘
typ └────────┘ ┴ └────────┘ ┴
406 computable (λ a, f (g a)) := hf.comp hg
id └────────┘ ┴ ┴ ┴ ┴ └┘└───┘ └┘
src └────────┘ └───┘
typ └────────┘ ┴ ┴ ┴ ┴ └┘└───┘ └┘
407
408 theorem comp₂ {f : γ → σ} {g : α → β → γ}
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
409 (hf : computable f) (hg : computable₂ g) :
id └────────┘ ┴ └─────────┘ ┴
src └────────┘ └─────────┘
typ └────────┘ ┴ └─────────┘ ┴
410 computable₂ (λ a b, f (g a b)) := hf.comp hg
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ └┘
src └─────────┘ └───┘
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ └┘
411
412 end computable
413
414 namespace computable₂
415 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {σ : Type*}
416 variables [primcodable α] [primcodable β] [primcodable γ] [primcodable δ] [primcodable σ]
id └─────────┘ └─────────┘ └─────────┘ └─────────┘ └─────────┘
src └─────────┘ └─────────┘ └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ └─────────┘ └─────────┘ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘ └─────────┘ └─────────┘ └─────────┘
417
418 theorem comp
419 {f : β → γ → σ} {g : α → β} {h : α → γ}
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
420 (hf : computable₂ f) (hg : computable g) (hh : computable h) :
id └─────────┘ ┴ └────────┘ ┴ └────────┘ ┴
src └─────────┘ └────────┘ └────────┘
typ └─────────┘ ┴ └────────┘ ┴ └────────┘ ┴
421 computable (λ a, f (g a) (h a)) := hf.comp (hg.pair hh)
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ └┘└───┘ └┘
src └────────┘ └───┘ └───┘
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ └┘└───┘ └┘
422
423 theorem comp₂
424 {f : γ → δ → σ} {g : α → β → γ} {h : α → β → δ}
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
425 (hf : computable₂ f) (hg : computable₂ g) (hh : computable₂ h) :
id └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴
426 computable₂ (λ a b, f (g a b) (h a b)) := hf.comp hg hh
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ └┘ └┘
src └─────────┘ └───┘
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ └┘ └┘
427
428 end computable₂
429
430 namespace partrec
431 variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
id ┴
typ ┴
432 variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
id └─────────┘ └─────────┘ └─────────┘ └─────────┘
src └─────────┘ └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ └─────────┘ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘ └─────────┘ └─────────┘
433
434 open computable
435
436 theorem rfind {p : α → ℕ →. bool} (hp : partrec₂ p) :
id ┴ ┴ └┘ └──┘ └──────┘ ┴
src ┴ └┘ └──┘ └──────┘
typ ┴ ┴ └┘ └──┘ └──────┘ ┴
doc └┘
437 partrec (λ a, nat.rfind (p a)) :=
id └─────┘ ┴ └───────┘ ┴ ┴
src └─────┘ └───────┘
typ └─────┘ ┴ └───────┘ ┴ ┴
438 (nat.partrec.rfind $ hp.map
id └───────────────┘ └┘└──┘
src └───────────────┘ └──┘
typ └───────────────┘ └┘└──┘
439 ((primrec.dom_bool (λ b, cond b 0 1))
id └──────────────┘ ┴ └──┘ ┴
src └──────────────┘ └──┘
typ └──────────────┘ ┴ └──┘ ┴
440 .comp primrec.snd).to₂.to_comp).of_eq $
id └──┘ └─────────┘ └─┘ └─────┘ └───┘
src └──┘ └─────────┘ └─┘ └─────┘ └───┘
typ └──┘ └─────────┘ └─┘ └─────┘ └───┘
441 λ n, begin
id ┴
typ ┴
st └─────
442 cases e : decode α n with a;
id └────┘ ┴ ┴
src └────┘ └─┘└────┘┴ ┴ └─────┘
typ └────┘ └─┘└────┘┴┴┴┴└─────┘
doc └────┘ └─┘ ┴ ┴ └─────┘
txt └────┘ └─┘ ┴ ┴ └─────┘
par └────┘ └─┘ ┴ ┴ └─────┘
pid ┴ └─┘ ┴ ┴ └─────┘
st ───────────────────────────────
443 simp [e, nat.rfind_zero_none, map_id'],
id ┴ └─────────────────┘ └─────┘
src └────┘ └┘└─────────────────┘└┘└─────┘┴
typ └────┘┴└┘└─────────────────┘└┘└─────┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st ─────────────────────────────────────────┘└─
444 congr, funext n,
src └───┘ └──────┘
typ └───┘ └──────┘
doc └──────┘
txt └───┘ └──────┘
par └───┘ └──────┘
pid └┘
st ──────┘└────────┘└─
445 simp [roption.map_map, (∘)],
id └─────────────┘ ┴
src └────┘└─────────────┘└┘┴└─┘
typ └────┘└─────────────┘└┘┴└─┘
doc └────┘ └┘ └─┘
txt └────┘ └┘ └─┘
par └────┘ └┘ └─┘
pid ┴┴ └┘ └─┘
st ────────────────────────────┘└─
446 apply map_id' (λ b, _),
id └─────┘
src └────┘└─────┘┴ └────┘
typ └────┘└─────┘┴ └────┘
doc └────┘ ┴ └────┘
txt └────┘ ┴ └────┘
par └────┘ ┴ └────┘
pid ┴ ┴ └────┘
st ───────────────────────┘└─
447 cases b; refl
id ┴
src └────┘ └───┘
typ └────┘┴ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st ───────────────┘
448 end
st └─┘
449
450 theorem rfind_opt {f : α → ℕ → option σ} (hf : computable₂ f) :
id ┴ ┴ └────┘ ┴ └─────────┘ ┴
src ┴ └────┘ └─────────┘
typ ┴ ┴ └────┘ ┴ └─────────┘ ┴
451 partrec (λ a, nat.rfind_opt (f a)) :=
id └─────┘ ┴ └───────────┘ ┴ ┴
src └─────┘ └───────────┘
typ └─────┘ ┴ └───────────┘ ┴ ┴
452 (rfind (primrec.option_is_some.to_comp.comp hf).part.to₂).bind
id └───┘ └────────────────────┘└──────┘└───┘ └┘ └──┘ └─┘ └──┘
src └───┘ └────────────────────┘└──────┘└───┘ └──┘ └─┘ └──┘
typ └───┘ └────────────────────┘└──────┘└───┘ └┘ └──┘ └─┘ └──┘
453 (of_option hf)
id └───────┘ └┘
src └───────┘
typ └───────┘ └┘
454
455 theorem nat_cases_right
456 {f : α → ℕ} {g : α → σ} {h : α → ℕ →. σ}
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └┘
457 (hf : computable f) (hg : computable g) (hh : partrec₂ h) :
id └────────┘ ┴ └────────┘ ┴ └──────┘ ┴
src └────────┘ └────────┘ └──────┘
typ └────────┘ ┴ └────────┘ ┴ └──────┘ ┴
458 partrec (λ a, (f a).cases (some (g a)) (h a)) :=
id └─────┘ ┴ ┴ ┴ └───┘ └──┘ ┴ ┴ ┴ ┴
src └─────┘ └───┘ └──┘
typ └─────┘ ┴ ┴ ┴ └───┘ └──┘ ┴ ┴ ┴ ┴
doc └──┘
459 (nat_elim hf hg (hh.comp fst (pred.comp $ hf.comp fst)).to₂).of_eq $
id └──────┘ └┘ └┘ └┘└───┘ └─┘ └──┘└───┘ └┘└───┘ └─┘ └─┘ └───┘
src └──────┘ └───┘ └─┘ └──┘└───┘ └───┘ └─┘ └─┘ └───┘
typ └──────┘ └┘ └┘ └┘└───┘ └─┘ └──┘└───┘ └┘└───┘ └─┘ └─┘ └───┘
460 λ a, begin
id ┴
typ ┴
st └─────
461 simp, cases f a; simp,
id ┴ ┴
src └──┘ └────┘ ┴ └──┘
typ └──┘ └────┘┴┴┴ └──┘
doc └──┘ └────┘ ┴ └──┘
txt └──┘ └────┘ ┴ └──┘
par └──┘ └────┘ ┴ └──┘
pid ┴ ┴
st ─────┘└───────────────┘└─
462 refine ext (λ b, ⟨λ H, _, λ H, _⟩),
id └─┘
src └─────┘└─┘┴ └──┘ └─────┘ └─────┘
typ └─────┘└─┘┴ └──┘ └─────┘ └─────┘
doc └─────┘└─┘┴ └──┘ └─────┘ └─────┘
txt └─────┘ ┴ └──┘ └─────┘ └─────┘
par └─────┘ ┴ └──┘ └─────┘ └─────┘
pid ┴ ┴ └──┘ └─────┘ └─────┘
st ───────────────────────────────────┘└─
463 { rcases mem_bind_iff.1 H with ⟨c, h₁, h₂⟩, exact h₂ },
id └──────────┘ ┴ └┘
src └─────┘└──────────┘└─┘ └───────────────┘ └────┘ ┴
typ └─────┘└──────────┘└─┘┴└───────────────┘ └────┘└┘┴
doc └─────┘ └─┘ └───────────────┘ └────┘ ┴
txt └─────┘ └─┘ └───────────────┘ └────┘ ┴
par └─────┘ └─┘ └───────────────┘ └────┘ ┴
pid ┴ └─┘ └───────────────┘ ┴ ┴
st ───┘└──────────────────────────────────────┘└─────────┘└┘└
464 { have : ∀ m, (nat.elim (roption.some (g a))
id └──────┘ └──────────┘ ┴
src └─────┘ └┘ ┴ └──────┘┴ └──────────┘┴ ┴ └──
typ └─────┘ └┘ ┴ └──────┘┴ └──────────┘┴ ┴┴ └──
doc └─────┘ └┘ ┴ ┴ └──────────┘┴ ┴ └──
txt └─────┘ └┘ ┴ ┴ ┴ ┴ └──
par └─────┘ └┘ ┴ ┴ ┴ ┴ └──
pid └───┘└┘ └┘ ┴ ┴ ┴ ┴ └──
st ───────────────────────────────────────────────
465 (λ y IH, IH.bind (λ _, h a n)) m).dom,
id └───┘ ┴ ┴ ┴
src ─────┘ └─────┘ └───┘┴ └──┘ ┴ ┴ └─┘ └───┘
typ ─────┘ └─────┘ └───┘┴ └──┘┴┴┴┴┴└─┘ └───┘
doc ─────┘ └─────┘ └───┘┴ └──┘ ┴ ┴ └─┘ └───┘
txt ─────┘ └─────┘ ┴ └──┘ ┴ ┴ └─┘ └───┘
par ─────┘ └─────┘ ┴ └──┘ ┴ ┴ └─┘ └───┘
pid ─────┘ └─────┘ ┴ └──┘ ┴ ┴ └─┘ └──┘┴
st ──────────────────────────────────────────┘└─
466 { intro, induction m; simp [*, H.fst] },
id ┴
src └───┘ └────────┘ └───────┘ └┘
typ └───┘ └────────┘┴ └───────┘└───┘└┘
doc └───┘ └────────┘ └───────┘ └┘
txt └───┘ └────────┘ └───────┘ └┘
par └───┘ └────────┘ └───────┘ └┘
pid ┴ ┴└──┘ ┴┴
st ─────┘└───┘└─────────────────────────────┘└┘└
467 exact ⟨⟨this n, H.fst⟩, H.snd⟩ }
id └──┘ ┴ └───┘ └───┘
src └────┘ ┴ └┘└───┘└─┘└───┘└┘
typ └────┘ └──┘┴┴└┘└───┘└─┘└───┘└┘
doc └────┘ ┴ └┘ └─┘ └┘
txt └────┘ ┴ └┘ └─┘ └┘
par └────┘ ┴ └┘ └─┘ └┘
pid ┴ ┴ └┘ └─┘ ┴┴
st ──────────────────────────────────┘└─
468 end
st ──┘
469
470 theorem bind_decode2_iff {f : α →. σ} : partrec f ↔
id ┴ └┘ ┴ └─────┘ ┴ ┴
src └┘ └─────┘ ┴
typ ┴ └┘ ┴ └─────┘ ┴ ┴
doc └┘
471 nat.partrec (λ n, roption.bind (decode2 α n) (λ a, (f a).map encode)) :=
id └─────────┘ ┴ └──────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘
src └─────────┘ └──────────┘ └─────┘ └─┘ └────┘
typ └─────────┘ ┴ └──────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘
doc └──────────┘ └─┘
472 ⟨λ hf, nat_iff.1 $ (of_option primrec.decode2.to_comp).bind $
id └┘ └─────┘┴ └───────┘ └─────────────┘└──────┘ └──┘
src └─────┘┴ └───────┘ └─────────────┘└──────┘ └──┘
typ └┘ └─────┘┴ └───────┘ └─────────────┘└──────┘ └──┘
473 (map hf (computable.encode.comp snd).to₂).comp snd,
id └─┘ └┘ └───────────────┘└───┘ └─┘ └─┘ └──┘ └─┘
src └─┘ └───────────────┘└───┘ └─┘ └─┘ └──┘ └─┘
typ └─┘ └┘ └───────────────┘└───┘ └─┘ └─┘ └──┘ └─┘
474 λ h, map_encode_iff.1 $ by simpa [encodek2]
id ┴ └────────────┘┴ └──────┘
src └────────────┘┴ └─────┘└──────┘└─
typ ┴ └────────────┘┴ └─────┘└──────┘└─
doc └─────┘ └─
txt └─────┘ └─
par └─────┘ └─
pid ┴┴ ┴└
st └─────────────────
475 using (nat_iff.2 h).comp (@computable.encode α _)⟩
id └─────┘ ┴ └───────────────┘ ┴
src ───────┘ └─────┘└─┘ └─────┘ └───────────────┘┴ └─┘
typ ───────┘ └─────┘└─┘┴└─────┘ └───────────────┘┴┴└─┘
doc ───────┘ └─┘ └─────┘ ┴ └─┘
txt ───────┘ └─┘ └─────┘ ┴ └─┘
par ───────┘ └─┘ └─────┘ ┴ └─┘
pid ─┘└────┘ └─┘ └─────┘ ┴ └─┘
st ──────────────────────────────────────────────────┘
476
477 theorem vector_m_of_fn : ∀ {n} {f : fin n → α →. σ}, (∀ i, partrec (f i)) →
id ┴┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └─────┘ ┴ ┴
src └─┘ └┘ └─────┘
typ ┴┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └─────┘ ┴ ┴
doc └┘
478 partrec (λ (a : α), vector.m_of_fn (λ i, f i a))
id └─────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴
src └─────┘ └────────────┘
typ └─────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴
479 | 0 f hf := const _
id └───┘
src └───┘
typ └───┘
480 | (n+1) f hf := by simp [vector.m_of_fn]; exact
id ┴ └────────────┘
src ┴ └────┘└────────────┘┴ └─────
typ ┴ └────┘└────────────┘┴ └─────
doc └────┘ ┴ └─────
txt └────┘ ┴ └─────
par └────┘ ┴ └─────
pid ┴┴ ┴ └
st └─────────────────────────────
481 (hf 0).bind (partrec.bind ((vector_m_of_fn (λ i, hf i.succ)).comp fst)
id └──────────┘ └────────────┘ └┘ └───┘
src ─┘ └───────┘ └──────────┘┴ ┴ └──┘ ┴ └───┘└──────┘ └─
typ ─┘ └───────┘ └──────────┘┴ └────────────┘┴ └──┘└┘┴ └───┘└──────┘ └─
doc ─┘ └───────┘ ┴ ┴ └──┘ ┴ └──────┘ └─
txt ─┘ └───────┘ ┴ ┴ └──┘ ┴ └──────┘ └─
par ─┘ └───────┘ ┴ ┴ └──┘ ┴ └──────┘ └─
pid ─┘ └───────┘ ┴ ┴ └──┘ ┴ └──────┘ └─
st ─────────────────────────────────────────────────────────────────────────
482 (primrec.vector_cons.to_comp.comp (snd.comp fst) snd))
id └──────────────────────────────┘ └──────┘ └─┘ └─┘
src ───┘ └──────────────────────────────┘┴ └──────┘┴└─┘└┘└─┘└──
typ ───┘ └──────────────────────────────┘┴ └──────┘┴└─┘└┘└─┘└──
doc ───┘ ┴ ┴ └┘ └──
txt ───┘ ┴ ┴ └┘ └──
par ───┘ ┴ ┴ └┘ └──
pid ───┘ ┴ ┴ └┘ └┘└
st ───────────────────────────────────────────────────────────
483
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
484 end partrec
485
486 @[simp] theorem vector.m_of_fn_roption_some {α n} : ∀ (f : fin n → α),
id └─┘ ┴ ┴ ┴
src └─┘
typ └─┘ ┴ ┴ ┴
doc └──┘
487 vector.m_of_fn (λ i, roption.some (f i)) = roption.some (vector.of_fn f) :=
id └────────────┘ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ └──────────┘ ┴
src └────────────┘ └──────────┘ ┴ └──────────┘ └──────────┘
typ └────────────┘ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ └──────────┘ ┴
doc └──────────┘ └──────────┘
488 vector.m_of_fn_pure
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
489
490 namespace computable
491 variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
492 variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
id └─────────┘ └─────────┘ └─────────┘ └─────────┘
src └─────────┘ └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ └─────────┘ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘ └─────────┘ └─────────┘
493
494 theorem option_some_iff {f : α → σ} : computable (λ a, some (f a)) ↔ computable f :=
id ┴ ┴ └────────┘ ┴ └──┘ ┴ ┴ ┴ └────────┘ ┴
src └────────┘ └──┘ ┴ └────────┘
typ ┴ ┴ └────────┘ ┴ └──┘ ┴ ┴ ┴ └────────┘ ┴
495 ⟨λ h, encode_iff.1 $ primrec.pred.to_comp.comp $ encode_iff.2 h,
id ┴ └────────┘┴ └──────────┘└──────┘└───┘ └────────┘┴ ┴
src └────────┘┴ └──────────┘└──────┘└───┘ └────────┘┴
typ ┴ └────────┘┴ └──────────┘└──────┘└───┘ └────────┘┴ ┴
496 option_some.comp⟩
id └─────────┘└───┘
src └─────────┘└───┘
typ └─────────┘└───┘
497
498 theorem bind_decode_iff {f : α → β → option σ} : computable₂ (λ a n,
id ┴ ┴ └────┘ ┴ └─────────┘ ┴ ┴
src └────┘ └─────────┘
typ ┴ ┴ └────┘ ┴ └─────────┘ ┴ ┴
499 (decode β n).bind (f a)) ↔ computable₂ f :=
id └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └─────────┘ ┴
src └────┘ └──┘ ┴ └─────────┘
typ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └─────────┘ ┴
500 ⟨λ hf, nat.partrec.of_eq
id └┘ └───────────────┘
src └───────────────┘
typ └┘ └───────────────┘
501 (((partrec.nat_iff.2 (nat.partrec.ppred.comp $
id └─────────────┘┴ └───────────────┘└───┘
src └─────────────┘┴ └───────────────┘└───┘
typ └─────────────┘┴ └───────────────┘└───┘
502 nat.partrec.of_primrec $ primcodable.prim β)).comp snd).bind
id └────────────────────┘ └──────────────┘ ┴ └──┘ └─┘ └──┘
src └────────────────────┘ └──────────────┘ └──┘ └─┘ └──┘
typ └────────────────────┘ └──────────────┘ ┴ └──┘ └─┘ └──┘
503 (computable.comp hf fst).to₂.part) $
id └─────────────┘ └┘ └─┘ └─┘ └──┘
src └─────────────┘ └─┘ └─┘ └──┘
typ └─────────────┘ └┘ └─┘ └─┘ └──┘
504 λ n, by simp;
id ┴
src └──┘
typ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └──────
505 cases decode α n.unpair.1; simp;
id └────┘ ┴ └──────┘
src └────┘└────┘┴ ┴└──────┘└┘ └──┘
typ └────┘└────┘┴┴┴└──────┘└┘ └──┘
doc └────┘ ┴ ┴└──────┘└┘ └──┘
txt └────┘ ┴ ┴ └┘ └──┘
par └────┘ ┴ ┴ └┘ └──┘
pid ┴ ┴ ┴ └┘
st ─────────────────────────────────────
506 cases decode β n.unpair.2; simp,
id └────┘ ┴ └──────┘
src └────┘└────┘┴ ┴└──────┘└┘ └──┘
typ └────┘└────┘┴┴┴└──────┘└┘ └──┘
doc └────┘ ┴ ┴└──────┘└┘ └──┘
txt └────┘ ┴ ┴ └┘ └──┘
par └────┘ ┴ ┴ └┘ └──┘
pid ┴ ┴ ┴ └┘
st ──────────────────────────────────┘
507 λ hf, begin
id └┘
typ └┘
st └─────
508 have : partrec (λ a : α × ℕ, (encode (decode β a.2)).cases
id └─────┘ ┴ ┴ └────┘
src └─────┘└─────┘┴ └───┘ ┴┴┴ └┘ └────┘┴ ┴ ┴ └──────────
typ └─────┘└─────┘┴ └───┘┴┴┴┴ └┘ └────┘┴ ┴ ┴ └──────────
doc └─────┘ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └──────────
txt └─────┘ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └──────────
par └─────┘ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └──────────
pid └───┘└┘ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └──────────
st ─────────────────────────────────────────────────────────────
509 (some option.none) (λ n, roption.map (f a.1) (decode β n))) :=
id └──┘ └─────────┘ └─────────┘ ┴ └────┘ ┴
src ───┘ └──┘┴└─────────┘└┘ └──┘└─────────┘┴ ┴ └──┘ └────┘┴ ┴ └──────
typ ───┘ └──┘┴└─────────┘└┘ └──┘└─────────┘┴ ┴┴ └──┘ └────┘┴┴┴ └──────
doc ───┘ └──┘┴ └┘ └──┘└─────────┘┴ ┴ └──┘ ┴ ┴ └──────
txt ───┘ ┴ └┘ └──┘ ┴ ┴ └──┘ ┴ ┴ └──────
par ───┘ ┴ └┘ └──┘ ┴ ┴ └──┘ ┴ ┴ └──────
pid ───┘ ┴ └┘ └──┘ ┴ ┴ └──┘ ┴ ┴ └─┘└───
st ───────────────────────────────────────────────────────────────────
510 partrec.nat_cases_right (primrec.encdec.to_comp.comp snd)
id └─────────────────────┘ └─────────────────────────┘
src ─┘└─────────────────────┘┴ └─────────────────────────┘┴ └─
typ ─┘└─────────────────────┘┴ └─────────────────────────┘┴ └─
doc ─┘ ┴ ┴ └─
txt ─┘ ┴ ┴ └─
par ─┘ ┴ ┴ └─
pid ─┘ ┴ ┴ └─
st ────────────────────────────────────────────────────────────
511 (const none) ((of_option (computable.decode.comp snd)).map
id └───┘ └──┘ └───────┘ └────────────────────┘
src ───┘ └───┘┴└──┘└┘ └───────┘┴ └────────────────────┘┴ └──────
typ ───┘ └───┘┴└──┘└┘ └───────┘┴ └────────────────────┘┴ └──────
doc ───┘ ┴ └┘ ┴ ┴ └──────
txt ───┘ ┴ └┘ ┴ ┴ └──────
par ───┘ ┴ └┘ ┴ ┴ └──────
pid ───┘ ┴ └┘ ┴ ┴ └──────
st ───────────────────────────────────────────────────────────────
512 (hf.comp (fst.comp $ fst.comp fst) snd).to₂),
id └─────┘ └──────┘ └─┘ └─┘
src ─────┘ └─────┘┴ ┴ ┴└──────┘┴└─┘└┘└─┘└────┘
typ ─────┘ └─────┘┴ ┴ ┴└──────┘┴└─┘└┘└─┘└────┘
doc ─────┘ ┴ ┴ ┴ ┴ └┘ └────┘
txt ─────┘ ┴ ┴ ┴ ┴ └┘ └────┘
par ─────┘ ┴ ┴ ┴ ┴ └┘ └────┘
pid ─────┘ ┴ ┴ ┴ ┴ └┘ └────┘
st ─────────────────────────────────────────────────┘└─
513 refine this.of_eq (λ a, _),
id └────────┘
src └─────┘└────────┘┴ └────┘
typ └─────┘└────────┘┴ └────┘
doc └─────┘ ┴ └────┘
txt └─────┘ ┴ └────┘
par └─────┘ ┴ └────┘
pid ┴ ┴ └────┘
st ───────────────────────────┘└─
514 simp, cases decode β a.2; simp [encodek]
id └────┘ ┴ ┴ └─────┘
src └──┘ └────┘└────┘┴ ┴ └┘ └────┘└─────┘└┘
typ └──┘ └────┘└────┘┴┴┴┴└┘ └────┘└─────┘└┘
doc └──┘ └────┘ ┴ ┴ └┘ └────┘ └┘
txt └──┘ └────┘ ┴ ┴ └┘ └────┘ └┘
par └──┘ └────┘ ┴ ┴ └┘ └────┘ └┘
pid ┴ ┴ ┴ └┘ ┴┴ ┴┴
st ─────┘└───────────────────────────────────┘
515 end⟩
st └─┘
516
517 theorem map_decode_iff {f : α → β → σ} : computable₂ (λ a n,
id ┴ ┴ ┴ └─────────┘ ┴ ┴
src └─────────┘
typ ┴ ┴ ┴ └─────────┘ ┴ ┴
518 (decode β n).map (f a)) ↔ computable₂ f :=
id └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─────────┘ ┴
src └────┘ └─┘ ┴ └─────────┘
typ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─────────┘ ┴
519 bind_decode_iff.trans option_some_iff
id └─────────────┘└────┘ └─────────────┘
src └─────────────┘└────┘ └─────────────┘
typ └─────────────┘└────┘ └─────────────┘
520
521 theorem nat_elim
522 {f : α → ℕ} {g : α → σ} {h : α → ℕ × σ → σ}
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
523 (hf : computable f) (hg : computable g) (hh : computable₂ h) :
id └────────┘ ┴ └────────┘ ┴ └─────────┘ ┴
src └────────┘ └────────┘ └─────────┘
typ └────────┘ ┴ └────────┘ ┴ └─────────┘ ┴
524 computable (λ a, (f a).elim (g a) (λ y IH, h a (y, IH))) :=
id └────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴┴ └┘
src └────────┘ └──┘ ┴
typ └────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴┴ └┘
525 (partrec.nat_elim hf hg hh.part).of_eq $
id └──────────────┘ └┘ └┘ └┘└───┘ └───┘
src └──────────────┘ └───┘ └───┘
typ └──────────────┘ └┘ └┘ └┘└───┘ └───┘
526 λ a, by simp; induction f a; simp *
id ┴ ┴ ┴
src └──┘ └────────┘ ┴ └──────
typ ┴ └──┘ └────────┘┴┴┴ └──────
doc └──┘ └────────┘ ┴ └──────
txt └──┘ └────────┘ ┴ └──────
par └──┘ └────────┘ ┴ └──────
pid ┴ ┴ ┴┴└
st └────────────────────────────
527
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
528 theorem nat_cases {f : α → ℕ} {g : α → σ} {h : α → ℕ → σ}
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
529 (hf : computable f) (hg : computable g) (hh : computable₂ h) :
id └────────┘ ┴ └────────┘ ┴ └─────────┘ ┴
src └────────┘ └────────┘ └─────────┘
typ └────────┘ ┴ └────────┘ ┴ └─────────┘ ┴
530 computable (λ a, (f a).cases (g a) (h a)) :=
id └────────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src └────────┘ └───┘
typ └────────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
531 nat_elim hf hg (hh.comp fst $ fst.comp snd).to₂
id └──────┘ └┘ └┘ └┘└───┘ └─┘ └─┘└───┘ └─┘ └─┘
src └──────┘ └───┘ └─┘ └─┘└───┘ └─┘ └─┘
typ └──────┘ └┘ └┘ └┘└───┘ └─┘ └─┘└───┘ └─┘ └─┘
532
533 theorem cond {c : α → bool} {f : α → σ} {g : α → σ}
id ┴ └──┘ ┴ ┴ ┴ ┴
src └──┘
typ ┴ └──┘ ┴ ┴ ┴ ┴
534 (hc : computable c) (hf : computable f) (hg : computable g) :
id └────────┘ ┴ └────────┘ ┴ └────────┘ ┴
src └────────┘ └────────┘ └────────┘
typ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴
535 computable (λ a, cond (c a) (f a) (g a)) :=
id └────────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └──┘
typ └────────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
536 (nat_cases (encode_iff.2 hc) hg (hf.comp fst).to₂).of_eq $
id └───────┘ └────────┘┴ └┘ └┘ └┘└───┘ └─┘ └─┘ └───┘
src └───────┘ └────────┘┴ └───┘ └─┘ └─┘ └───┘
typ └───────┘ └────────┘┴ └┘ └┘ └┘└───┘ └─┘ └─┘ └───┘
537 λ a, by cases c a; refl
id ┴ ┴ ┴
src └────┘ ┴ └────
typ ┴ └────┘┴┴┴ └────
doc └────┘ ┴ └────
txt └────┘ ┴ └────
par └────┘ ┴ └────
pid ┴ ┴ └
st └────────────────
538
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
539 theorem option_cases {o : α → option β} {f : α → σ} {g : α → β → σ}
id ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘
typ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
540 (ho : computable o) (hf : computable f) (hg : computable₂ g) :
id └────────┘ ┴ └────────┘ ┴ └─────────┘ ┴
src └────────┘ └────────┘ └─────────┘
typ └────────┘ ┴ └────────┘ ┴ └─────────┘ ┴
541 @computable _ σ _ _ (λ a, option.cases_on (o a) (f a) (g a)) :=
id └────────┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └─────────────┘
typ └────────┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
542 option_some_iff.1 $
id └─────────────┘┴
src └─────────────┘┴
typ └─────────────┘┴
543 (nat_cases (encode_iff.2 ho) (option_some_iff.2 hf)
id └───────┘ └────────┘┴ └┘ └─────────────┘┴ └┘
src └───────┘ └────────┘┴ └─────────────┘┴
typ └───────┘ └────────┘┴ └┘ └─────────────┘┴ └┘
544 (map_decode_iff.2 hg)).of_eq $
id └────────────┘┴ └┘ └───┘
src └────────────┘┴ └───┘
typ └────────────┘┴ └┘ └───┘
545 λ a, by cases o a; simp [encodek]; refl
id ┴ ┴ ┴ └─────┘
src └────┘ ┴ └────┘└─────┘┴ └────
typ ┴ └────┘┴┴┴ └────┘└─────┘┴ └────
doc └────┘ ┴ └────┘ ┴ └────
txt └────┘ ┴ └────┘ ┴ └────
par └────┘ ┴ └────┘ ┴ └────
pid ┴ ┴ ┴┴ ┴ └
st └────────────────────────────────
546
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
547 theorem option_bind {f : α → option β} {g : α → β → option σ}
id ┴ └────┘ ┴ ┴ ┴ └────┘ ┴
src └────┘ └────┘
typ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴
548 (hf : computable f) (hg : computable₂ g) :
id └────────┘ ┴ └─────────┘ ┴
src └────────┘ └─────────┘
typ └────────┘ ┴ └─────────┘ ┴
549 computable (λ a, (f a).bind (g a)) :=
id └────────┘ ┴ ┴ ┴ └──┘ ┴ ┴
src └────────┘ └──┘
typ └────────┘ ┴ ┴ ┴ └──┘ ┴ ┴
550 (option_cases hf (const option.none) hg).of_eq $
id └──────────┘ └┘ └───┘ └─────────┘ └┘ └───┘
src └──────────┘ └───┘ └─────────┘ └───┘
typ └──────────┘ └┘ └───┘ └─────────┘ └┘ └───┘
551 λ a, by cases f a; refl
id ┴ ┴ ┴
src └────┘ ┴ └────
typ ┴ └────┘┴┴┴ └────
doc └────┘ ┴ └────
txt └────┘ ┴ └────
par └────┘ ┴ └────
pid ┴ ┴ └
st └────────────────
552
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
553 theorem option_map {f : α → option β} {g : α → β → σ}
id ┴ └────┘ ┴ ┴ ┴ ┴
src └────┘
typ ┴ └────┘ ┴ ┴ ┴ ┴
554 (hf : computable f) (hg : computable₂ g) : computable (λ a, (f a).map (g a)) :=
id └────────┘ ┴ └─────────┘ ┴ └────────┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └────────┘ └─────────┘ └────────┘ └─┘
typ └────────┘ ┴ └─────────┘ ┴ └────────┘ ┴ ┴ ┴ └─┘ ┴ ┴
555 option_bind hf (option_some.comp₂ hg)
id └─────────┘ └┘ └─────────┘└────┘ └┘
src └─────────┘ └─────────┘└────┘
typ └─────────┘ └┘ └─────────┘└────┘ └┘
556
557 theorem sum_cases
558 {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ}
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
559 (hf : computable f) (hg : computable₂ g) (hh : computable₂ h) :
id └────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴
src └────────┘ └─────────┘ └─────────┘
typ └────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴
560 @computable _ σ _ _ (λ a, sum.cases_on (f a) (g a) (h a)) :=
id └────────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └──────────┘
typ └────────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
561 option_some_iff.1 $
id └─────────────┘┴
src └─────────────┘┴
typ └─────────────┘┴
562 (cond (nat_bodd.comp $ encode_iff.2 hf)
id └──┘ └──────┘└───┘ └────────┘┴ └┘
src └──┘ └──────┘└───┘ └────────┘┴
typ └──┘ └──────┘└───┘ └────────┘┴ └┘
563 (option_map (computable.decode.comp $ nat_div2.comp $ encode_iff.2 hf) hh)
id └────────┘ └───────────────┘└───┘ └──────┘└───┘ └────────┘┴ └┘ └┘
src └────────┘ └───────────────┘└───┘ └──────┘└───┘ └────────┘┴
typ └────────┘ └───────────────┘└───┘ └──────┘└───┘ └────────┘┴ └┘ └┘
564 (option_map (computable.decode.comp $ nat_div2.comp $ encode_iff.2 hf) hg)).of_eq $
id └────────┘ └───────────────┘└───┘ └──────┘└───┘ └────────┘┴ └┘ └┘ └───┘
src └────────┘ └───────────────┘└───┘ └──────┘└───┘ └────────┘┴ └───┘
typ └────────┘ └───────────────┘└───┘ └──────┘└───┘ └────────┘┴ └┘ └┘ └───┘
565 λ a, by cases f a with b c;
id ┴ ┴ ┴
src └────┘ ┴ └───────┘
typ ┴ └────┘┴┴┴└───────┘
doc └────┘ ┴ └───────┘
txt └────┘ ┴ └───────┘
par └────┘ ┴ └───────┘
pid ┴ ┴ └───────┘
st └────────────────────
566 simp [nat.div2_bit, nat.bodd_bit, encodek]; refl
id └──────────┘ └──────────┘ └─────┘
src └────┘└──────────┘└┘└──────────┘└┘└─────┘┴ └────
typ └────┘└──────────┘└┘└──────────┘└┘└─────┘┴ └────
doc └────┘ └┘ └┘ ┴ └────
txt └────┘ └┘ └┘ ┴ └────
par └────┘ └┘ └┘ ┴ └────
pid ┴┴ └┘ └┘ ┴ └
st ───────────────────────────────────────────────────
567
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
568 theorem nat_strong_rec
569 (f : α → ℕ → σ) {g : α → list σ → option σ} (hg : computable₂ g)
id ┴ ┴ ┴ ┴ └──┘ ┴ └────┘ ┴ └─────────┘ ┴
src ┴ └──┘ └────┘ └─────────┘
typ ┴ ┴ ┴ ┴ └──┘ ┴ └────┘ ┴ └─────────┘ ┴
570 (H : ∀ a n, g a ((list.range n).map (f a)) = some (f a n)) : computable₂ f :=
id ┴ ┴ ┴ ┴ └────────┘ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └─────────┘ ┴
src └────────┘ └─┘ ┴ └──┘ └─────────┘
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └─────────┘ ┴
571 suffices computable₂ (λ a n, (list.range n).map (f a)), from
id └─────────┘ ┴ ┴ └────────┘ ┴ └─┘ ┴ ┴
src └─────────┘ └────────┘ └─┘
typ └─────────┘ ┴ ┴ └────────┘ ┴ └─┘ ┴ ┴
572 option_some_iff.1 $
id └─────────────┘┴
src └─────────────┘┴
typ └─────────────┘┴
573 (list_nth.comp (this.comp fst (succ.comp snd)) snd).to₂.of_eq $
id └──────┘└───┘ └──┘└───┘ └─┘ └──┘└───┘ └─┘ └─┘ └─┘ └───┘
src └──────┘└───┘ └───┘ └─┘ └──┘└───┘ └─┘ └─┘ └─┘ └───┘
typ └──────┘└───┘ └──┘└───┘ └─┘ └──┘└───┘ └─┘ └─┘ └─┘ └───┘
574 λ a, by simp [list.nth_range (nat.lt_succ_self a.2)]; refl,
id ┴ └────────────┘ └──────────────┘ ┴
src └────┘└────────────┘┴ └──────────────┘┴ └──┘ └──┘
typ ┴ └────┘└────────────┘┴ └──────────────┘┴┴└──┘ └──┘
doc └────┘ ┴ ┴ └──┘ └──┘
txt └────┘ ┴ ┴ └──┘ └──┘
par └────┘ ┴ ┴ └──┘ └──┘
pid ┴┴ ┴ ┴ └──┘
st └─────────────────────────────────────────────────┘
575 option_some_iff.1 $
id └─────────────┘┴
src └─────────────┘┴
typ └─────────────┘┴
576 (nat_elim snd (const (option.some [])) (to₂ $
id └──────┘ └─┘ └───┘ └─────────┘ └┘ └─┘
src └──────┘ └─┘ └───┘ └─────────┘ └┘ └─┘
typ └──────┘ └─┘ └───┘ └─────────┘ └┘ └─┘
577 option_bind (snd.comp snd) $ to₂ $
id └─────────┘ └─┘└───┘ └─┘ └─┘
src └─────────┘ └─┘└───┘ └─┘ └─┘
typ └─────────┘ └─┘└───┘ └─┘ └─┘
578 option_map
id └────────┘
src └────────┘
typ └────────┘
579 (hg.comp (fst.comp $ fst.comp fst) snd)
id └┘└───┘ └─┘└───┘ └─┘└───┘ └─┘ └─┘
src └───┘ └─┘└───┘ └─┘└───┘ └─┘ └─┘
typ └┘└───┘ └─┘└───┘ └─┘└───┘ └─┘ └─┘
580 (to₂ $ list_concat.comp (snd.comp fst) snd))).of_eq $
id └─┘ └─────────┘└───┘ └─┘└───┘ └─┘ └─┘ └───┘
src └─┘ └─────────┘└───┘ └─┘└───┘ └─┘ └─┘ └───┘
typ └─┘ └─────────┘└───┘ └─┘└───┘ └─┘ └─┘ └───┘
581 λ a, begin
id ┴
typ ┴
st └─────
582 simp, induction a.2 with n IH, {refl},
id ┴
src └──┘ └────────┘ └──────────┘ └──┘
typ └──┘ └────────┘┴└──────────┘ └──┘
doc └──┘ └────────┘ └──────────┘ └──┘
txt └──┘ └────────┘ └──────────┘ └──┘
par └──┘ └────────┘ └──────────┘ └──┘
pid ┴ └─┘└───────┘
st ─────┘└───────────────────────┘└─────┘└┘└
583 simp [IH, H, list.range_concat]
id └┘ ┴ └───────────────┘
src └────┘ └┘ └┘└───────────────┘└┘
typ └────┘└┘└┘┴└┘└───────────────┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
st ─────────────────────────────────┘
584 end
st └─┘
585
586 theorem list_of_fn : ∀ {n} {f : fin n → α → σ},
id ┴┴ └─┘ ┴ ┴ ┴ ┴
src └─┘
typ ┴┴ └─┘ ┴ ┴ ┴ ┴
587 (∀ i, computable (f i)) → computable (λ a, list.of_fn (λ i, f i a))
id ┴ └────────┘ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └────────┘
typ ┴ └────────┘ ┴ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
588 | 0 f hf := const []
id └───┘ └┘
src └───┘ └┘
typ └───┘ └┘
589 | (n+1) f hf := by simp [list.of_fn_succ]; exact
id ┴ └─────────────┘
src ┴ └────┘└─────────────┘┴ └─────
typ ┴ └────┘└─────────────┘┴ └─────
doc └────┘ ┴ └─────
txt └────┘ ┴ └─────
par └────┘ ┴ └─────
pid ┴┴ ┴ └
st └──────────────────────────────
590 list_cons.comp (hf 0) (list_of_fn (λ i, hf i.succ))
id └────────────┘ └────────┘ └┘ └───┘
src ─┘└────────────┘┴ └──┘ ┴ └──┘ ┴ └───┘└──
typ ─┘└────────────┘┴ └──┘ └────────┘┴ └──┘└┘┴ └───┘└──
doc ─┘ ┴ └──┘ ┴ └──┘ ┴ └──
txt ─┘ ┴ └──┘ ┴ └──┘ ┴ └──
par ─┘ ┴ └──┘ ┴ └──┘ ┴ └──
pid ─┘ ┴ └──┘ ┴ └──┘ ┴ └┘└
st ──────────────────────────────────────────────────────
591
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
592 theorem vector_of_fn {n} {f : fin n → α → σ}
id └─┘ ┴ ┴ ┴
src └─┘
typ └─┘ ┴ ┴ ┴
593 (hf : ∀ i, computable (f i)) : computable (λ a, vector.of_fn (λ i, f i a)) :=
id ┴ └────────┘ ┴ ┴ └────────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └──────────┘
typ ┴ └────────┘ ┴ ┴ └────────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴
594 (partrec.vector_m_of_fn hf).of_eq $ λ a, by simp
id └────────────────────┘ └┘ └───┘ ┴
src └────────────────────┘ └───┘ └────
typ └────────────────────┘ └┘ └───┘ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
595
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
596 end computable
597
598 namespace partrec
599 variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
id ┴
typ ┴
600 variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
id └─────────┘ └─────────┘ └─────────┘ └─────────┘
src └─────────┘ └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ └─────────┘ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘ └─────────┘ └─────────┘
601
602 open computable
603
604 theorem option_some_iff {f : α →. σ} :
id ┴ └┘ ┴
src └┘
typ ┴ └┘ ┴
doc └┘
605 partrec (λ a, (f a).map option.some) ↔ partrec f :=
id └─────┘ ┴ ┴ ┴ └─┘ └─────────┘ ┴ └─────┘ ┴
src └─────┘ └─┘ └─────────┘ ┴ └─────┘
typ └─────┘ ┴ ┴ ┴ └─┘ └─────────┘ ┴ └─────┘ ┴
doc └─┘
606 ⟨λ h, (nat.partrec.ppred.comp h).of_eq $
id ┴ └───────────────┘└───┘ ┴ └───┘
src └───────────────┘└───┘ └───┘
typ ┴ └───────────────┘└───┘ ┴ └───┘
607 λ n, by simp [roption.bind_assoc, bind_some_eq_map],
id ┴ └────────────────┘ └──────────────┘
src └────┘└────────────────┘└┘└──────────────┘┴
typ ┴ └────┘└────────────────┘└┘└──────────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └──────────────────────────────────────────┘
608 λ hf, hf.map (option_some.comp snd).to₂⟩
id └┘ └┘└──┘ └─────────┘└───┘ └─┘ └─┘
src └──┘ └─────────┘└───┘ └─┘ └─┘
typ └┘ └┘└──┘ └─────────┘└───┘ └─┘ └─┘
609
610 theorem option_cases_right {o : α → option β} {f : α → σ} {g : α → β →. σ}
id ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src └────┘ └┘
typ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └┘
611 (ho : computable o) (hf : computable f) (hg : partrec₂ g) :
id └────────┘ ┴ └────────┘ ┴ └──────┘ ┴
src └────────┘ └────────┘ └──────┘
typ └────────┘ ┴ └────────┘ ┴ └──────┘ ┴
612 @partrec _ σ _ _ (λ a, option.cases_on (o a) (some (f a)) (g a)) :=
id └─────┘ ┴ ┴ └─────────────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └─────┘ └─────────────┘ └──┘
typ └─────┘ ┴ ┴ └─────────────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘
613 have partrec (λ (a : α), nat.cases (roption.some (f a))
id └─────┘ ┴ └───────┘ └──────────┘ ┴ ┴
src └─────┘ └───────┘ └──────────┘
typ └─────┘ ┴ └───────┘ └──────────┘ ┴ ┴
doc └──────────┘
614 (λ n, roption.bind (decode β n) (g a)) (encode (o a))) :=
id ┴ └──────────┘ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
src └──────────┘ └────┘ └────┘
typ ┴ └──────────┘ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
doc └──────────┘
615 nat_cases_right (encode_iff.2 ho) hf.part $
id └─────────────┘ └────────┘┴ └┘ └┘└───┘
src └─────────────┘ └────────┘┴ └───┘
typ └─────────────┘ └────────┘┴ └┘ └┘└───┘
616 ((@computable.decode β _).comp snd).of_option.bind
id └───────────────┘ ┴ └──┘ └─┘ └───────┘ └──┘
src └───────────────┘ └──┘ └─┘ └───────┘ └──┘
typ └───────────────┘ ┴ └──┘ └─┘ └───────┘ └──┘
617 (hg.comp (fst.comp fst) snd).to₂,
id └┘└───┘ └─┘└───┘ └─┘ └─┘ └─┘
src └───┘ └─┘└───┘ └─┘ └─┘ └─┘
typ └┘└───┘ └─┘└───┘ └─┘ └─┘ └─┘
618 this.of_eq $ λ a, by cases o a with b; simp [encodek]
id └──┘└────┘ ┴ ┴ ┴ └─────┘
src └────┘ └────┘ ┴ └─────┘ └────┘└─────┘└─
typ └──┘└────┘ ┴ └────┘┴┴┴└─────┘ └────┘└─────┘└─
doc └────┘ ┴ └─────┘ └────┘ └─
txt └────┘ ┴ └─────┘ └────┘ └─
par └────┘ ┴ └─────┘ └────┘ └─
pid ┴ ┴ └─────┘ ┴┴ ┴└
st └─────────────────────────────────
619
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
620 theorem sum_cases_right
621 {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ →. σ}
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └┘
622 (hf : computable f) (hg : computable₂ g) (hh : partrec₂ h) :
id └────────┘ ┴ └─────────┘ ┴ └──────┘ ┴
src └────────┘ └─────────┘ └──────┘
typ └────────┘ ┴ └─────────┘ ┴ └──────┘ ┴
623 @partrec _ σ _ _ (λ a, sum.cases_on (f a) (λ b, some (g a b)) (h a)) :=
id └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──────────┘ └──┘
typ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
624 have partrec (λ a, (option.cases_on
id └─────┘ ┴ └─────────────┘
src └─────┘ └─────────────┘
typ └─────┘ ┴ └─────────────┘
625 (sum.cases_on (f a) (λ b, option.none) option.some : option γ)
id └──────────┘ ┴ ┴ ┴ └─────────┘ └─────────┘ └────┘ ┴
src └──────────┘ └─────────┘ └─────────┘ └────┘
typ └──────────┘ ┴ ┴ ┴ └─────────┘ └─────────┘ └────┘ ┴
626 (some (sum.cases_on (f a) (λ b, some (g a b))
id └──┘ └──────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ └──────────┘ └──┘
typ └──┘ └──────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘
627 (λ c, option.none)))
id ┴ └─────────┘
src └─────────┘
typ ┴ └─────────┘
628 (λ c, (h a c).map option.some) : roption (option σ))) :=
id ┴ ┴ ┴ ┴ └─┘ └─────────┘ └─────┘ └────┘ ┴
src └─┘ └─────────┘ └─────┘ └────┘
typ ┴ ┴ ┴ ┴ └─┘ └─────────┘ └─────┘ └────┘ ┴
doc └─┘ └─────┘
629 option_cases_right
id └────────────────┘
src └────────────────┘
typ └────────────────┘
630 (sum_cases hf (const option.none).to₂ (option_some.comp snd).to₂)
id └───────┘ └┘ └───┘ └─────────┘ └─┘ └─────────┘└───┘ └─┘ └─┘
src └───────┘ └───┘ └─────────┘ └─┘ └─────────┘└───┘ └─┘ └─┘
typ └───────┘ └┘ └───┘ └─────────┘ └─┘ └─────────┘└───┘ └─┘ └─┘
631 (sum_cases hf (option_some.comp hg) (const option.none).to₂)
id └───────┘ └┘ └─────────┘└───┘ └┘ └───┘ └─────────┘ └─┘
src └───────┘ └─────────┘└───┘ └───┘ └─────────┘ └─┘
typ └───────┘ └┘ └─────────┘└───┘ └┘ └───┘ └─────────┘ └─┘
632 (option_some_iff.2 hh),
id └─────────────┘┴ └┘
src └─────────────┘┴
typ └─────────────┘┴ └┘
633 option_some_iff.1 $ this.of_eq $ λ a, by cases f a; simp
id └─────────────┘┴ └──┘└────┘ ┴ ┴ ┴
src └─────────────┘┴ └────┘ └────┘ ┴ └────
typ └─────────────┘┴ └──┘└────┘ ┴ └────┘┴┴┴ └────
doc └────┘ ┴ └────
txt └────┘ ┴ └────
par └────┘ ┴ └────
pid ┴ ┴ └
st └────────────────
634
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
635 theorem sum_cases_left
636 {f : α → β ⊕ γ} {g : α → β →. σ} {h : α → γ → σ}
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └┘
637 (hf : computable f) (hg : partrec₂ g) (hh : computable₂ h) :
id └────────┘ ┴ └──────┘ ┴ └─────────┘ ┴
src └────────┘ └──────┘ └─────────┘
typ └────────┘ ┴ └──────┘ ┴ └─────────┘ ┴
638 @partrec _ σ _ _ (λ a, sum.cases_on (f a) (g a) (λ c, some (h a c))) :=
id └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └─────┘ └──────────┘ └──┘
typ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘
639 (sum_cases_right (sum_cases hf
id └─────────────┘ └───────┘ └┘
src └─────────────┘ └───────┘
typ └─────────────┘ └───────┘ └┘
640 (sum_inr.comp snd).to₂ (sum_inl.comp snd).to₂) hh hg).of_eq $
id └─────┘└───┘ └─┘ └─┘ └─────┘└───┘ └─┘ └─┘ └┘ └┘ └───┘
src └─────┘└───┘ └─┘ └─┘ └─────┘└───┘ └─┘ └─┘ └───┘
typ └─────┘└───┘ └─┘ └─┘ └─────┘└───┘ └─┘ └─┘ └┘ └┘ └───┘
641 λ a, by cases f a; simp
id ┴ ┴ ┴
src └────┘ ┴ └────
typ ┴ └────┘┴┴┴ └────
doc └────┘ ┴ └────
txt └────┘ ┴ └────
par └────┘ ┴ └────
pid ┴ ┴ └
st └────────────────
642
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
643 private lemma fix_aux
644 {f : α →. σ ⊕ α} (hf : partrec f)
id ┴ └┘ ┴ ┴ ┴ └─────┘ ┴
src └┘ ┴ └─────┘
typ ┴ └┘ ┴ ┴ ┴ └─────┘ ┴
doc └┘
645 (a : α) (b : σ) :
id ┴ ┴
typ ┴ ┴
646 let F : α → ℕ →. σ ⊕ α := λ a n,
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └┘
647 n.elim (some (sum.inr a)) $ λ y IH, IH.bind $ λ s,
id ┴└───┘ └──┘ └─────┘ ┴ ┴ └┘ └┘└───┘ ┴
src └───┘ └──┘ └─────┘ └───┘
typ ┴└───┘ └──┘ └─────┘ ┴ ┴ └┘ └┘└───┘ ┴
doc └──┘ └───┘
648 sum.cases_on s (λ _, roption.some s) f in
id └──────────┘ ┴ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ ┴ └──────────┘ ┴ ┴
doc └──────────┘
649 (∃ (n : ℕ), ((∃ (b' : σ), sum.inl b' ∈ F a n) ∧
id ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴ ┴ ┴ ┴
650 ∀ {m : ℕ}, m < n → (∃ (b : α), sum.inr b ∈ F a m)) ∧
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └─────┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
651 sum.inl b ∈ F a n) ↔ b ∈ pfun.fix f a :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
src └─────┘ ┴ ┴ ┴ └──────┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
652 begin
st └─────
653 intro, refine ⟨λ h, _, λ h, _⟩,
src └───┘ └─────┘ └─────┘ └────┘
typ └───┘ └─────┘ └─────┘ └────┘
doc └───┘ └─────┘ └─────┘ └────┘
txt └───┘ └─────┘ └─────┘ └────┘
par └───┘ └─────┘ └─────┘ └────┘
pid ┴ └─────┘ └────┘
st ──────┘└───────────────────────┘└─
654 { rcases h with ⟨n, ⟨_x, h₁⟩, h₂⟩,
id ┴
src └─────┘ └─────────────────────┘
typ └─────┘┴└─────────────────────┘
doc └─────┘ └─────────────────────┘
txt └─────┘ └─────────────────────┘
par └─────┘ └─────────────────────┘
pid ┴ └─────────────────────┘
st ───┘└─────────────────────────────┘└─
655 have : ∀ m a' (_: sum.inr a' ∈ F a m)
id └─────┘ ┴ ┴
src └─────┘ └────────┘└─────┘┴ ┴┴┴ ┴ ┴ └─
typ └─────┘ └────────┘└─────┘┴ ┴┴┴┴┴ ┴ └─
doc └─────┘ └────────┘ ┴ ┴ ┴ ┴ ┴ └─
txt └─────┘ └────────┘ ┴ ┴ ┴ ┴ ┴ └─
par └─────┘ └────────┘ ┴ ┴ ┴ ┴ ┴ └─
pid └───┘└┘ └────────┘ ┴ ┴ ┴ ┴ ┴ └─
st ──────────────────────────────────────────
656 (_: b ∈ pfun.fix f a'), b ∈ pfun.fix f a,
id ┴ ┴ └──────┘ ┴ ┴
src ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──────┘┴ ┴
typ ─────────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴└──────┘┴┴┴┴
doc ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────┘└─
657 { intros m a' am ba,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └─────────┘
st ─────┘└───────────────┘└─
658 induction m with m IH generalizing a'; simp [F] at am,
id ┴ ┴
src └────────┘ └────────────────────────┘ └────┘ └─────┘
typ └────────┘┴└────────────────────────┘ └────┘┴└─────┘
doc └────────┘ └────────────────────────┘ └────┘ └─────┘
txt └────────┘ └────────────────────────┘ └────┘ └─────┘
par └────────┘ └────────────────────────┘ └────┘ └─────┘
pid ┴ ┴└───────┘└──────────────┘ ┴┴ ┴┴└───┘
st ──────────────────────────────────────────────────────────┘└─
659 { rwa ← am },
id └┘
src └────┘ ┴
typ └────┘└┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid └─┘ ┴
st ───────┘└───────┘└┘└
660 rcases am with ⟨a₂, am₂, fa₂⟩,
id └┘
src └─────┘ └──────────────────┘
typ └─────┘└┘└──────────────────┘
doc └─────┘ └──────────────────┘
txt └─────┘ └──────────────────┘
par └─────┘ └──────────────────┘
pid ┴ └──────────────────┘
st ──────────────────────────────────┘└─
661 exact IH _ am₂ (pfun.mem_fix_iff.2 (or.inr ⟨_, fa₂, ba⟩)) },
id └┘ └─┘ └──────────────┘ └────┘ └─┘ └┘
src └────┘ └─┘ ┴ └──────────────┘└─┘ └────┘┴ └─┘ └┘ └──┘
typ └────┘└┘└─┘└─┘┴ └──────────────┘└─┘ └────┘┴ └─┘└─┘└┘└┘└──┘
doc └────┘ └─┘ ┴ └─┘ ┴ └─┘ └┘ └──┘
txt └────┘ └─┘ ┴ └─┘ ┴ └─┘ └┘ └──┘
par └────┘ └─┘ ┴ └─┘ ┴ └─┘ └┘ └──┘
pid ┴ └─┘ ┴ └─┘ ┴ └─┘ └┘ └─┘┴
st ───────────────────────────────────────────────────────────────┘└┘└
662 cases n; simp [F] at h₂, {cases h₂},
id ┴ ┴ └┘
src └────┘ └────┘ └─────┘ └────┘
typ └────┘┴ └────┘┴└─────┘ └────┘└┘
doc └────┘ └────┘ └─────┘ └────┘
txt └────┘ └────┘ └─────┘ └────┘
par └────┘ └────┘ └─────┘ └────┘
pid ┴ ┴┴ ┴┴└───┘ ┴
st ──────────────────────────┘└─────────┘└┘└
663 rcases h₂ with h₂ | ⟨a', am', fa'⟩,
id └┘
src └─────┘ └───────────────────────┘
typ └─────┘└┘└───────────────────────┘
doc └─────┘ └───────────────────────┘
txt └─────┘ └───────────────────────┘
par └─────┘ └───────────────────────┘
pid ┴ └───────────────────────┘
st ─────────────────────────────────────┘└─
664 { cases h₁ (nat.lt_succ_self _) with a' h,
id └┘ └──────────────┘
src └────┘ ┴ └──────────────┘└───────────┘
typ └────┘└┘┴ └──────────────┘└───────────┘
doc └────┘ ┴ └───────────┘
txt └────┘ ┴ └───────────┘
par └────┘ ┴ └───────────┘
pid ┴ ┴ └─┘└────────┘
st ─────┘└─────────────────────────────────────┘└─
665 injection mem_unique h h₂ },
id └────────┘ ┴ └┘
src └────────┘└────────┘┴ ┴ ┴
typ └────────┘└────────┘┴┴┴└┘┴
doc └────────┘ ┴ ┴ ┴
txt └────────┘ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───────────────────────────────┘└┘└
666 { exact this _ _ am' (pfun.mem_fix_iff.2 (or.inl fa')) } },
id └──┘ └─┘ └──────────────┘ └────┘ └─┘
src └────┘ └───┘ ┴ └──────────────┘└─┘ └────┘┴ └─┘
typ └────┘└──┘└───┘└─┘┴ └──────────────┘└─┘ └────┘┴└─┘└─┘
doc └────┘ └───┘ ┴ └─┘ ┴ └─┘
txt └────┘ └───┘ ┴ └─┘ ┴ └─┘
par └────┘ └───┘ ┴ └─┘ ┴ └─┘
pid ┴ └───┘ ┴ └─┘ ┴ └┘┴
st ──────────────────────────────────────────────────────────┘└──┘└
667 { suffices : ∀ a' (_: b ∈ pfun.fix f a') k (_: sum.inr a' ∈ F a k),
id ┴ └──────┘ ┴ ┴
src └─────────┘ └──────┘ ┴ ┴└──────┘┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └
typ └─────────┘ └──────┘ ┴┴┴└──────┘┴┴┴ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ └
doc └─────────┘ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └
txt └─────────┘ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └
par └─────────┘ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └
pid └───────┘└┘ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └
st ──────────────────────────────────────────────────────────────────────
668 ∃ n, sum.inl b ∈ F a n ∧
id └─────┘ ┴
src ──────┘ └┘ ┴└─────┘┴ ┴ ┴ ┴ ┴ ┴ └
typ ──────┘ └┘ ┴└─────┘┴┴┴ ┴ ┴ ┴ ┴ └
doc ──────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
txt ──────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
par ──────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
pid ──────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
st ────────────────────────────────
669 ∀ (m < n) (_ : k ≤ m), ∃ a₂, sum.inr a₂ ∈ F a m,
id ┴ ┴ ┴ └─────┘ ┴ ┴
src ────────┘ └────┘ └─────┘ ┴┴┴ ┴ ┴┴└─┘┴┴└─────┘┴ ┴ ┴ ┴ ┴
typ ────────┘ └────┘ └─────┘ ┴┴┴ ┴ ┴┴└─┘┴┴└─────┘┴ ┴ ┴┴┴┴┴
doc ────────┘ └────┘ └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
txt ────────┘ └────┘ └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
par ────────┘ └────┘ └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ────────┘ └────┘ └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
670 { rcases this _ h 0 (by simp [F]) with ⟨n, hn₁, hn₂⟩,
id └──┘ ┴ ┴
src └─────┘ └─┘ └─┘ ┴└────┘ ┴└──────────────────┘
typ └─────┘└──┘└─┘┴└─┘ ┴└────┘┴┴└──────────────────┘
doc └─────┘ └─┘ └─┘ ┴└────┘ ┴└──────────────────┘
txt └─────┘ └─┘ └─┘ ┴└────┘ ┴└──────────────────┘
par └─────┘ └─┘ └─┘ ┴└────┘ ┴└──────────────────┘
pid ┴ └─┘ └─┘ └─────┘ └───────────────────┘
st ─────┘└───────────────────┘└───────┘└──────────────────┘└─
671 exact ⟨_, ⟨⟨_, hn₁⟩, λ m mn, hn₂ m mn (nat.zero_le _)⟩, hn₁⟩ },
id └─┘ └─────────┘ └─┘
src └────┘ └─┘ └─┘ └─┘ └─────┘ ┴ ┴ ┴ └─────────┘└────┘ └┘
typ └────┘ └─┘ └─┘ └─┘ └─────┘└─┘┴ ┴ ┴ └─────────┘└────┘└─┘└┘
doc └────┘ └─┘ └─┘ └─┘ └─────┘ ┴ ┴ ┴ └────┘ └┘
txt └────┘ └─┘ └─┘ └─┘ └─────┘ ┴ ┴ ┴ └────┘ └┘
par └────┘ └─┘ └─┘ └─┘ └─────┘ ┴ ┴ ┴ └────┘ └┘
pid ┴ └─┘ └─┘ └─┘ └─────┘ ┴ ┴ ┴ └────┘ ┴┴
st ──────────────────────────────────────────────────────────────────┘└┘└
672 intros a₁ h₁,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └────┘
st ───────────────┘└─
673 apply pfun.fix_induction h₁, intros a₂ h₂ IH k hk,
id └────────────────┘ └┘
src └────┘└────────────────┘┴ └──────────────────┘
typ └────┘└────────────────┘┴└┘ └──────────────────┘
doc └────┘ ┴ └──────────────────┘
txt └────┘ ┴ └──────────────────┘
par └────┘ ┴ └──────────────────┘
pid ┴ ┴ └────────────┘
st ──────────────────────────────┘└────────────────────┘└─
674 rcases pfun.mem_fix_iff.1 h₂ with h₂ | ⟨a₃, am₃, fa₃⟩,
id └──────────────┘ └┘
src └─────┘└──────────────┘└─┘ └───────────────────────┘
typ └─────┘└──────────────┘└─┘└┘└───────────────────────┘
doc └─────┘ └─┘ └───────────────────────┘
txt └─────┘ └─┘ └───────────────────────┘
par └─────┘ └─┘ └───────────────────────┘
pid ┴ └─┘ └───────────────────────┘
st ────────────────────────────────────────────────────────┘└─
675 { refine ⟨k.succ, _, λ m mk km, ⟨a₂, _⟩⟩,
id └────┘ └┘
src └─────┘ └────┘└───┘ └────────┘ └───┘
typ └─────┘ └────┘└───┘ └────────┘ └┘└───┘
doc └─────┘ └───┘ └────────┘ └───┘
txt └─────┘ └───┘ └────────┘ └───┘
par └─────┘ └───┘ └────────┘ └───┘
pid ┴ └───┘ └────────┘ └───┘
st ─────┘└────────────────────────────────────┘└─
676 { simp [F], exact or.inr ⟨_, hk, h₂⟩ },
id ┴ └────┘ └┘ └┘
src └────┘ ┴ └────┘└────┘┴ └─┘ └┘ └┘
typ └────┘┴┴ └────┘└────┘┴ └─┘└┘└┘└┘└┘
doc └────┘ ┴ └────┘ ┴ └─┘ └┘ └┘
txt └────┘ ┴ └────┘ ┴ └─┘ └┘ └┘
par └────┘ ┴ └────┘ ┴ └─┘ └┘ └┘
pid ┴┴ ┴ ┴ ┴ └─┘ └┘ ┴┴
st ───────┘└──────┘└─────────────────────────┘└┘└
677 { rwa le_antisymm (nat.le_of_lt_succ mk) km } },
id └─────────┘ └───────────────┘ └┘ └┘
src └──┘└─────────┘┴ └───────────────┘┴ └┘ ┴
typ └──┘└─────────┘┴ └───────────────┘┴└┘└┘└┘┴
doc └──┘ ┴ ┴ └┘ ┴
txt └──┘ ┴ ┴ └┘ ┴
par └──┘ ┴ ┴ └┘ ┴
pid ┴ ┴ ┴ └┘ ┴
st ─────────────────────────────────────────────────┘└──┘└
678 { rcases IH _ fa₃ am₃ k.succ _ with ⟨n, hn₁, hn₂⟩,
id └┘ └─┘ └─┘ └────┘
src └─────┘ └─┘ ┴ ┴└────┘└───────────────────┘
typ └─────┘└┘└─┘└─┘┴└─┘┴└────┘└───────────────────┘
doc └─────┘ └─┘ ┴ ┴ └───────────────────┘
txt └─────┘ └─┘ ┴ ┴ └───────────────────┘
par └─────┘ └─┘ ┴ ┴ └───────────────────┘
pid ┴ └─┘ ┴ ┴ └───────────────────┘
st ────────────────────────────────────────────────────┘└─
679 { refine ⟨n, hn₁, λ m mn km, _⟩,
id ┴ └─┘
src └─────┘ └┘ └┘ └──────────┘
typ └─────┘ ┴└┘└─┘└┘ └──────────┘
doc └─────┘ └┘ └┘ └──────────┘
txt └─────┘ └┘ └┘ └──────────┘
par └─────┘ └┘ └┘ └──────────┘
pid ┴ └┘ └┘ └──────────┘
st ───────┘└───────────────────────────┘└─
680 cases lt_or_eq_of_le km with km km,
id └────────────┘ └┘
src └────┘└────────────┘┴ └─────────┘
typ └────┘└────────────┘┴└┘└─────────┘
doc └────┘ ┴ └─────────┘
txt └────┘ ┴ └─────────┘
par └────┘ ┴ └─────────┘
pid ┴ ┴ └─────────┘
st ─────────────────────────────────────────┘└─
681 { exact hn₂ _ mn km },
id └─┘ └┘ └┘
src └────┘ └─┘ ┴ ┴
typ └────┘└─┘└─┘└┘┴└┘┴
doc └────┘ └─┘ ┴ ┴
txt └────┘ └─┘ ┴ ┴
par └────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ─────────┘└────────────────┘└┘└
682 { exact km ▸ ⟨_, hk⟩ } },
id └┘ ┴ └┘
src └────┘ ┴┴┴ └─┘ └┘
typ └────┘└┘┴┴┴ └─┘└┘└┘
doc └────┘ ┴ ┴ └─┘ └┘
txt └────┘ ┴ ┴ └─┘ └┘
par └────┘ ┴ ┴ └─┘ └┘
pid ┴ ┴ ┴ └─┘ ┴┴
st ────────────────────────────┘└──┘└
683 { simp [F], exact ⟨_, hk, am₃⟩ } } }
id ┴ └┘ └─┘
src └────┘ ┴ └────┘ └─┘ └┘ └┘
typ └────┘┴┴ └────┘ └─┘└┘└┘└─┘└┘
doc └────┘ ┴ └────┘ └─┘ └┘ └┘
txt └────┘ ┴ └────┘ └─┘ └┘ └┘
par └────┘ ┴ └────┘ └─┘ └┘ └┘
pid ┴┴ ┴ ┴ └─┘ └┘ ┴┴
st ───────────────┘└───────────────────┘└─────
684 end
st ──┘
685
686 theorem fix
687 {f : α →. σ ⊕ α} (hf : partrec f) : partrec (pfun.fix f) :=
id ┴ └┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ └──────┘ ┴
src └┘ ┴ └─────┘ └─────┘ └──────┘
typ ┴ └┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ └──────┘ ┴
doc └┘
688 let F : α → ℕ →. σ ⊕ α := λ a n,
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └┘
689 n.elim (some (sum.inr a)) $ λ y IH, IH.bind $ λ s,
id ┴└───┘ └──┘ └─────┘ ┴ ┴ └┘ └┘└───┘ ┴
src └───┘ └──┘ └─────┘ └───┘
typ ┴└───┘ └──┘ └─────┘ ┴ ┴ └┘ └┘└───┘ ┴
doc └──┘ └───┘
690 sum.cases_on s (λ _, roption.some s) f in
id └──────────┘ ┴ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ ┴ └──────────┘ ┴ ┴
doc └──────────┘
691 have hF : partrec₂ F :=
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
692 partrec.nat_elim snd (sum_inr.comp fst).part
id └──────────────┘ └─┘ └─────┘└───┘ └─┘ └──┘
src └──────────────┘ └─┘ └─────┘└───┘ └─┘ └──┘
typ └──────────────┘ └─┘ └─────┘└───┘ └─┘ └──┘
693 (sum_cases_right (snd.comp snd)
id └─────────────┘ └─┘└───┘ └─┘
src └─────────────┘ └─┘└───┘ └─┘
typ └─────────────┘ └─┘└───┘ └─┘
694 (snd.comp $ snd.comp fst).to₂
id └─┘└───┘ └─┘└───┘ └─┘ └─┘
src └─┘└───┘ └─┘└───┘ └─┘ └─┘
typ └─┘└───┘ └─┘└───┘ └─┘ └─┘
695 (hf.comp snd).to₂).to₂,
id └┘└───┘ └─┘ └─┘ └─┘
src └───┘ └─┘ └─┘ └─┘
typ └┘└───┘ └─┘ └─┘ └─┘
696 let p := λ a n, @roption.map _ bool
id ┴ ┴ ┴ └─────────┘ └──┘
src └─────────┘ └──┘
typ ┴ ┴ ┴ └─────────┘ └──┘
doc └─────────┘
697 (λ s, sum.cases_on s (λ_, tt) (λ _, ff)) (F a n) in
id ┴ └──────────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴
src └──────────┘ └┘ └┘
typ ┴ └──────────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴
698 have hp : partrec₂ p := hF.map ((sum_cases computable.id
id └──────┘ ┴ └┘└──┘ └───────┘ └───────────┘
src └──────┘ └──┘ └───────┘ └───────────┘
typ └──────┘ ┴ └┘└──┘ └───────┘ └───────────┘
699 (const tt).to₂ (const ff).to₂).comp snd).to₂,
id └───┘ └┘ └─┘ └───┘ └┘ └─┘ └──┘ └─┘ └─┘
src └───┘ └┘ └─┘ └───┘ └┘ └─┘ └──┘ └─┘ └─┘
typ └───┘ └┘ └─┘ └───┘ └┘ └─┘ └──┘ └─┘ └─┘
700 (hp.rfind.bind (hF.bind
id └┘└────┘└───┘ └┘└───┘
src └────┘└───┘ └───┘
typ └┘└────┘└───┘ └┘└───┘
701 (sum_cases_right snd snd.to₂ none.to₂).to₂).to₂).of_eq $
id └─────────────┘ └─┘ └─┘└──┘ └──┘└──┘ └─┘ └─┘ └───┘
src └─────────────┘ └─┘ └─┘└──┘ └──┘└──┘ └─┘ └─┘ └───┘
typ └─────────────┘ └─┘ └─┘└──┘ └──┘└──┘ └─┘ └─┘ └───┘
702 λ a, ext $ λ b, by simp; apply fix_aux hf
id ┴ └─┘ ┴ └─────┘ └┘
src └─┘ └──┘ └────┘└─────┘┴ └
typ ┴ └─┘ ┴ └──┘ └────┘└─────┘┴└┘└
doc └─┘ └──┘ └────┘ ┴ └
txt └──┘ └────┘ ┴ └
par └──┘ └────┘ ┴ └
pid ┴ ┴ └
st └───────────────────────
703
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
704 end partrec